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

Metamath Proof Explorer

Theorem com45

Description: Commutation of antecedents. Swap 4th and 5th. Deduction associated with com34 . Double deduction associated with com23 . Triple deduction associated with com12 . (Contributed by Jeff Hankins, 28-Jun-2009)

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

Proof

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