Theorem 3impia

Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)

Hypothesis
3impia.1
\( \vdash \varphi \wedge \psi \rightarrow \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
Proof
3impia.1
expimpd _
3impib _