conb>i

Theorem.

Arguments:

phi (pr), psi (pr),

Hypotheses:

(phileftrightarrowlnotpsi)

Assertions:

(psileftrightarrowlnotphi)

Proof:

Hyp Ref Line Expr
Hypo1(phileftrightarrowlnotpsi)
1bicomi2(lnotpsileftrightarrowphi)
2conb<i3(lnotphileftrightarrowpsi)
3bicomi4(psileftrightarrowlnotphi)