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

Metamath Proof Explorer

Theorem mpsyl

Description: Modus ponens combined with a syllogism inference. (Contributed by Alan Sare, 20-Apr-2011)

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

Proof

Step Hyp Ref Expression
1 mpsyl.1 ⊢ φ
2 mpsyl.2 ⊢ ψ → χ
3 mpsyl.3 ⊢ φ → χ → θ
4 1 a1i ⊢ ψ → φ
5 4 2 3 sylc ⊢ ψ → θ