bmpg<

Theorem.

Arguments:

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

Hypotheses:

psi
(phileftrightarrowforallxpsi)

Assertions:

phi

Proof:

Hyp Ref Line Expr
Hypo1psi
2(phileftrightarrowforallxpsi)
2bi<3(forallxpsitophi)
1, 3mpg4phi