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 φψθ