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

Metamath Proof Explorer

Theorem com52l

Description: Commutation of antecedents. Rotate left twice. (Contributed by Jeff Hankins, 28-Jun-2009)

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

Proof

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