Theorem imdistand

Distribution of implication with conjunction (deduction form). (Contributed by NM, 27-Aug-2004.)

Hypothesis
imdistand.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \psi \wedge \chi \rightarrow \psi \wedge \theta \)
Proof
l0
imdistand.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \)
imdistan
\( \vdash \psi \rightarrow \chi \rightarrow \theta \leftrightarrow \psi \wedge \chi \rightarrow \psi \wedge \theta \)
sylib l0 _