Theorem com23

Commutation of antecedents. Swap 2nd and 3rd. Deduction associated with com12. (Contributed by NM, 27-Dec-1992.) (Proof shortened by Wolf Lammen, 4-Aug-2012.)

Hypothesis
com3.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \chi \rightarrow \psi \rightarrow \theta \)
Proof
l0
com3.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \)
pm2.27
\( \vdash \chi \rightarrow (\chi \rightarrow \theta) \rightarrow \theta \)
syl9 l0 _