Theorem dfnan2

Alternative denial in terms of our primitive connectives (implication and negation). (Contributed by WL, 26-Jun-2020.)

Conclusion
\( \vdash \varphi \barwedge \psi \leftrightarrow \varphi \rightarrow \neg \psi \)
Proof
l0
df-nan
\( \vdash \varphi \barwedge \psi \leftrightarrow \neg (\varphi \wedge \psi) \)
imnan
\( \vdash \varphi \rightarrow \neg \psi \leftrightarrow \neg (\varphi \wedge \psi) \)
bitr4i l0 _