an.nim

Theorem.

Arguments:

phi (pr), psi (pr),

Assertions:

((phiwedgelnotpsi)leftrightarrowlnot(phitopsi))

Proof:

Hyp Ref Line Expr
im.an1((phitopsi)leftrightarrowlnot(phiwedgelnotpsi))
1conb>i2((phiwedgelnotpsi)leftrightarrowlnot(phitopsi))