exn.al

Theorem.

Arguments:

x (sv), phi (pr),

Assertions:

(existsxlnotphileftrightarrowlnotforallxphi)

Proof:

Hyp Ref Line Expr
al.ex1(forallxphileftrightarrowlnotexistsxlnotphi)
1conb>i2(existsxlnotphileftrightarrowlnotforallxphi)