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

Metamath Proof Explorer

Theorem syl5com

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

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

Proof

Step Hyp Ref Expression
1 syl5com.1 ⊢ φ → ψ
2 syl5com.2 ⊢ χ → ψ → θ
3 1 a1d ⊢ φ → χ → ψ
4 3 2 sylcom ⊢ φ → χ → θ