Theorem com34

Commutation of antecedents. Swap 3rd and 4th. Deduction associated with com23. Double deduction associated with com12. (Contributed by NM, 25-Apr-1994.)

Hypothesis
com4.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \rightarrow \tau \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \theta \rightarrow \chi \rightarrow \tau \)
Proof
l0
com4.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \rightarrow \tau \)
pm2.04
\( \vdash (\chi \rightarrow \theta \rightarrow \tau) \rightarrow \theta \rightarrow \chi \rightarrow \tau \)
syl6 l0 _