Metamath Proof Explorer


Theorem sylcom

Description: Syllogism inference with commutation of antecedents. (Contributed by NM, 29-Aug-2004) (Proof shortened by Mel L. O'Cat, 2-Feb-2006) (Proof shortened by Stefan Allan, 23-Feb-2006)

Ref Expression
Hypotheses sylcom.1 φ ψ χ
sylcom.2 ψ χ θ
Assertion sylcom φ ψ θ

Proof

Step Hyp Ref Expression
1 sylcom.1 φ ψ χ
2 sylcom.2 ψ χ θ
3 2 a2i ψ χ ψ θ
4 1 3 syl φ ψ θ