Theorem nic-dfneg

This theorem "defines" negation in terms of 'nand'. Analogous to nannot. In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to a definition ($a statement). (Contributed by NM, 11-Dec-2008.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash ((\varphi \barwedge \varphi) \barwedge \neg \varphi) \barwedge (((\varphi \barwedge \varphi) \barwedge (\varphi \barwedge \varphi)) \barwedge (\neg \varphi \barwedge \neg \varphi)) \)
Proof
nannot
l1
bicomi _
\( \vdash \varphi \barwedge \varphi \leftrightarrow \neg \varphi \)
nanbi
\( \vdash \varphi \barwedge \varphi \leftrightarrow \neg \varphi \leftrightarrow ((\varphi \barwedge \varphi) \barwedge \neg \varphi) \barwedge (((\varphi \barwedge \varphi) \barwedge (\varphi \barwedge \varphi)) \barwedge (\neg \varphi \barwedge \neg \varphi)) \)
mpbi l1 _