>bii

Theorem.

Arguments:

phi (pr), psi (pr),

Hypotheses:

(psitophi)
(phitopsi)

Assertions:

(phileftrightarrowpsi)

Proof:

Hyp Ref Line Expr
Hypo1(psitophi)
2(phitopsi)
1, 2>bi3(phileftrightarrowpsi)