Theorem com45

Commutation of antecedents. Swap 4th and 5th. Deduction associated with com34. Double deduction associated with com23. Triple deduction associated with com12. (Contributed by Jeff Hankins, 28-Jun-2009.)

Hypothesis
com5.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \rightarrow \tau \rightarrow \eta \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \tau \rightarrow \theta \rightarrow \eta \)
Proof
l0
com5.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \rightarrow \tau \rightarrow \eta \)
pm2.04
\( \vdash (\theta \rightarrow \tau \rightarrow \eta) \rightarrow \tau \rightarrow \theta \rightarrow \eta \)
syl8 l0 _