Theorem nan

Theorem to move a conjunct in and out of a negation. (Contributed by NM, 9-Nov-2003.)

Conclusion
\( \vdash \varphi \rightarrow \neg (\psi \wedge \chi) \leftrightarrow \varphi \wedge \psi \rightarrow \neg \chi \)
Proof
l0
impexp
\( \vdash \varphi \wedge \psi \rightarrow \neg \chi \leftrightarrow \varphi \rightarrow \psi \rightarrow \neg \chi \)
imnan
imbi2i _
\( \vdash \varphi \rightarrow \psi \rightarrow \neg \chi \leftrightarrow \varphi \rightarrow \neg (\psi \wedge \chi) \)
bitr2i l0 _