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

Metamath Proof Explorer

Theorem com4l

Description: Commutation of antecedents. Rotate left. (Contributed by NM, 25-Apr-1994) (Proof shortened by Mel L. O'Cat, 15-Aug-2004)

Ref Expression
Hypothesis com4.1 ⊢ φ → ψ → χ → θ → τ
Assertion com4l ⊢ ψ → χ → θ → φ → τ

Proof

Step Hyp Ref Expression
1 com4.1 ⊢ φ → ψ → χ → θ → τ
2 1 com3l ⊢ ψ → χ → φ → θ → τ
3 2 com34 ⊢ ψ → χ → θ → φ → τ