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

Metamath Proof Explorer

Theorem mpsylsyld

Description: Modus ponens combined with a double syllogism inference. (Contributed by Alan Sare, 22-Jul-2012)

Ref Expression
Hypotheses mpsylsyld.1 ⊢ 𝜑
mpsylsyld.2 ⊢ ( 𝜓 → ( 𝜒 → 𝜃 ) )
mpsylsyld.3 ⊢ ( 𝜑 → ( 𝜃 → 𝜏 ) )
Assertion mpsylsyld ( 𝜓 → ( 𝜒 → 𝜏 ) )

Proof

Step Hyp Ref Expression
1 mpsylsyld.1 ⊢ 𝜑
2 mpsylsyld.2 ⊢ ( 𝜓 → ( 𝜒 → 𝜃 ) )
3 mpsylsyld.3 ⊢ ( 𝜑 → ( 𝜃 → 𝜏 ) )
4 1 a1i ⊢ ( 𝜓 → 𝜑 )
5 4 2 3 sylsyld ⊢ ( 𝜓 → ( 𝜒 → 𝜏 ) )