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

Metamath Proof Explorer

Theorem mpisyl

Description: A syllogism combined with a modus ponens inference. (Contributed by Alan Sare, 25-Jul-2011)

Ref Expression
Hypotheses mpisyl.1 ⊢ φ → ψ
mpisyl.2 ⊢ χ
mpisyl.3 ⊢ ψ → χ → θ
Assertion mpisyl ⊢ φ → θ

Proof

Step Hyp Ref Expression
1 mpisyl.1 ⊢ φ → ψ
2 mpisyl.2 ⊢ χ
3 mpisyl.3 ⊢ ψ → χ → θ
4 2 3 mpi ⊢ ψ → θ
5 1 4 syl ⊢ φ → θ