exan.al

Theorem.

Arguments:

x (sv), phi (pr), psi (pr),

Assertions:

(existsx(phiwedgelnotpsi)leftrightarrowlnotforallx(phitopsi))

Proof:

Hyp Ref Line Expr
im.an1((phitopsi)leftrightarrowlnot(phiwedgelnotpsi))
1eqt-∀-i2(forallx(phitopsi)leftrightarrowforallxlnot(phiwedgelnotpsi))
aln.ex3(forallxlnot(phiwedgelnotpsi)leftrightarrowlnotexistsx(phiwedgelnotpsi))
2, 3bitr4(forallx(phitopsi)leftrightarrowlnotexistsx(phiwedgelnotpsi))
4conb>i5(existsx(phiwedgelnotpsi)leftrightarrowlnotforallx(phitopsi))