Theorem nannan

Nested alternative denials. (Contributed by Jeff Hoffman, 19-Nov-2007.) (Proof shortened by Wolf Lammen, 26-Jun-2020.)

Conclusion
\( \vdash \varphi \barwedge (\psi \barwedge \chi) \leftrightarrow \varphi \rightarrow \psi \wedge \chi \)
Proof
l0
dfnan2
\( \vdash \varphi \barwedge (\psi \barwedge \chi) \leftrightarrow \varphi \rightarrow \neg (\psi \barwedge \chi) \)
nanan
imbi2i _
\( \vdash \varphi \rightarrow \psi \wedge \chi \leftrightarrow \varphi \rightarrow \neg (\psi \barwedge \chi) \)
bitr4i l0 _