>nor

Theorem.

Arguments:

phi (pr), psi (pr),

Hypotheses:

lnotpsi
lnotphi

Assertions:

lnot(phiveepsi)

Proof:

Hyp Ref Line Expr
Hypo1lnotpsi
2lnotphi
1, 2>andi3(lnotphiwedgelnotpsi)
nor.an4(lnot(phiveepsi)leftrightarrow(lnotphiwedgelnotpsi))
3, 4bmp<5lnot(phiveepsi)