Theorem 3impdi

Importation inference (undistribute conjunction). (Contributed by NM, 14-Aug-1995.)

Hypothesis
3impdi.1
\( \vdash \varphi \wedge \psi \wedge (\varphi \wedge \chi) \rightarrow \theta \)
Conclusion
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
Proof
3impdi.1
anandis _
3impb _