bmpg>

Theorem.

Arguments:

x (sv), phi (pr), psi (pr),

Hypotheses:

phi
(forallxphileftrightarrowpsi)

Assertions:

psi

Proof:

Hyp Ref Line Expr
Hypo1phi
2(forallxphileftrightarrowpsi)
2bi>3(forallxphitopsi)
1, 3mpg4psi