an-false

Theorem.

Arguments:

phi (pr), psi (pr),

Assertions:

(lnotphito(phileftrightarrow(phiwedgepsi)))

Proof:

Hyp Ref Line Expr
<neg1(lnotphito(phito(phiwedgepsi)))
siman<2((phiwedgepsi)tophi)
2ax13(lnotphito((phiwedgepsi)tophi))
1, 3>bid4(lnotphito(phileftrightarrow(phiwedgepsi)))