Theorem imdistanda

Distribution of implication with conjunction (deduction version with conjoined antecedent). (Contributed by Jeff Madsen, 19-Jun-2011.)

Hypothesis
imdistanda.1
\( \vdash \varphi \wedge \psi \rightarrow \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \psi \wedge \chi \rightarrow \psi \wedge \theta \)
Proof
imdistanda.1
ex _
imdistand _