Theorem nanim

Implication in terms of alternative denial. (Contributed by Jeff Hoffman, 19-Nov-2007.)

Conclusion
\( \vdash \varphi \rightarrow \psi \leftrightarrow \varphi \barwedge (\psi \barwedge \psi) \)
Proof
l0
nannan
\( \vdash \varphi \barwedge (\psi \barwedge \psi) \leftrightarrow \varphi \rightarrow \psi \wedge \psi \)
anidmdbi
\( \vdash \varphi \rightarrow \psi \wedge \psi \leftrightarrow \varphi \rightarrow \psi \)
bitr2i l0 _