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

Metamath Proof Explorer

Theorem com25

Description: Commutation of antecedents. Swap 2nd and 5th. Deduction associated with com14 . (Contributed by Jeff Hankins, 28-Jun-2009)

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

Proof

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