This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem com5l

Description: Commutation of antecedents. Rotate left. (Contributed by Jeff Hankins, 28-Jun-2009) (Proof shortened by Wolf Lammen, 29-Jul-2012)

Ref Expression
Hypothesis com5.1 ⊢ φ → ψ → χ → θ → τ → η
Assertion com5l ⊢ ψ → χ → θ → τ → φ → η

Proof

Step Hyp Ref Expression
1 com5.1 ⊢ φ → ψ → χ → θ → τ → η
2 1 com4l ⊢ ψ → χ → θ → φ → τ → η
3 2 com45 ⊢ ψ → χ → θ → τ → φ → η