Theorem imdistanri

Distribution of implication with conjunction. (Contributed by NM, 8-Jan-2002.)

Hypothesis
imdistanri.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \psi \wedge \varphi \rightarrow \chi \wedge \varphi \)
Proof
imdistanri.1
com12 _
impac _