Theorem imdistan

Distribution of implication with conjunction. (Contributed by NM, 31-May-1999.) (Proof shortened by Wolf Lammen, 6-Dec-2012.)

Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \leftrightarrow \varphi \wedge \psi \rightarrow \varphi \wedge \chi \)
Proof
l0
pm5.42
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \leftrightarrow \varphi \rightarrow \psi \rightarrow \varphi \wedge \chi \)
impexp
\( \vdash \varphi \wedge \psi \rightarrow \varphi \wedge \chi \leftrightarrow \varphi \rightarrow \psi \rightarrow \varphi \wedge \chi \)
bitr4i l0 _