Theorem com5l

Commutation of antecedents. Rotate left. (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 \psi \rightarrow \chi \rightarrow \theta \rightarrow \tau \rightarrow \varphi \rightarrow \eta \)

Proof

com5.1

com4l _

com45 _