Theorem imdistani

Distribution of implication with conjunction. (Contributed by NM, 1-Aug-1994.)

Hypothesis
imdistani.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \wedge \psi \rightarrow \varphi \wedge \chi \)
Proof
imdistani.1
anc2li _
imp _