Theorem nannot

Negation in terms of alternative denial. (Contributed by Jeff Hoffman, 19-Nov-2007.) Use dfnan2. (Revised by Wolf Lammen, 26-Jun-2020.)

Conclusion
\( \vdash \neg \varphi \leftrightarrow \varphi \barwedge \varphi \)
Proof
l0
dfnan2
\( \vdash \varphi \barwedge \varphi \leftrightarrow \varphi \rightarrow \neg \varphi \)
pm4.8
\( \vdash \varphi \rightarrow \neg \varphi \leftrightarrow \neg \varphi \)
bitr2i l0 _