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

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