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

Metamath Proof Explorer

Theorem syl6com

Description: Syllogism inference with commuted antecedents. (Contributed by NM, 25-May-2005)

Ref Expression
Hypotheses syl6com.1 ⊢ φ → ψ → χ
syl6com.2 ⊢ χ → θ
Assertion syl6com ⊢ ψ → φ → θ

Proof

Step Hyp Ref Expression
1 syl6com.1 ⊢ φ → ψ → χ
2 syl6com.2 ⊢ χ → θ
3 1 2 syl6 ⊢ φ → ψ → θ
4 3 com12 ⊢ ψ → φ → θ