2false-eq

Theorem.

Arguments:

phi (pr), psi (pr),

Hypotheses:

lnotpsi
lnotphi

Assertions:

(phileftrightarrowpsi)

Proof:

Hyp Ref Line Expr
Hypo1lnotpsi
2lnotphi
false-eq3((lnotphiwedgelnotpsi)to(phileftrightarrowpsi))
1, 2, 3anmp<>4(phileftrightarrowpsi)