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

Metamath Proof Explorer

Theorem sylancom

Description: Syllogism inference with commutation of antecedents. (Contributed by NM, 2-Jul-2008)

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

Proof

Step Hyp Ref Expression
1 sylancom.1 ⊢ φ ∧ ψ → χ
2 sylancom.2 ⊢ χ ∧ ψ → θ
3 simpr ⊢ φ ∧ ψ → ψ
4 1 3 2 syl2anc ⊢ φ ∧ ψ → θ