Theorem com15

Commutation of antecedents. Swap 1st and 5th. (Contributed by Jeff Hankins, 28-Jun-2009.) (Proof shortened by Wolf Lammen, 29-Jul-2012.)

Hypothesis

com5.1

\( \vdash \varphi \rightarrow \psi \rightarrow \chi \rightarrow \theta \rightarrow \tau \rightarrow \eta \)

Conclusion

\( \vdash \tau \rightarrow \psi \rightarrow \chi \rightarrow \theta \rightarrow \varphi \rightarrow \eta \)

Proof

com5.1

com5l _

com4r _