Metamath Proof Explorer


Theorem sylancr

Description: Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Hypotheses sylancr.1 ψ
sylancr.2 φχ
sylancr.3 ψχθ
Assertion sylancr φθ

Proof

Step Hyp Ref Expression
1 sylancr.1 ψ
2 sylancr.2 φχ
3 sylancr.3 ψχθ
4 1 a1i φψ
5 4 2 3 syl2anc φθ