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