or.an

Theorem.

Arguments:

phi (pr), psi (pr),

Assertions:

((phiveepsi)leftrightarrowlnot(lnotphiwedgelnotpsi))

Proof:

Hyp Ref Line Expr
bneg>1((phiveepsi)leftrightarrowlnotlnot(phiveepsi))
nor.an2(lnot(phiveepsi)leftrightarrow(lnotphiwedgelnotpsi))
2bi.bldneg3(lnotlnot(phiveepsi)leftrightarrowlnot(lnotphiwedgelnotpsi))
1, 3bitr4((phiveepsi)leftrightarrowlnot(lnotphiwedgelnotpsi))