Theorem impcomd

Importation deduction with commuted antecedents. (Contributed by Peter Mazsa, 24-Sep-2022.) (Proof shortened by Wolf Lammen, 22-Oct-2022.)

Hypothesis
impd.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \chi \wedge \psi \rightarrow \theta \)
Proof
impd.1
com23 _
impd _