2true-eq

Theorem.

Arguments:

phi (pr), psi (pr),

Hypotheses:

psi
phi

Assertions:

(phileftrightarrowpsi)

Proof:

Hyp Ref Line Expr
Hypo1psi
2phi
1ax13(phitopsi)
2ax14(psitophi)
3, 4>bii5(phileftrightarrowpsi)