Theorem mpsyl

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

Hypotheses
mpsyl.1
\( \vdash \varphi \)
mpsyl.2
\( \vdash \psi \rightarrow \chi \)
mpsyl.3
\( \vdash \varphi \rightarrow \chi \rightarrow \theta \)
Conclusion
\( \vdash \psi \rightarrow \theta \)
Proof
mpsyl.1
l1
a1i _
\( \vdash \psi \rightarrow \varphi \)
l2
mpsyl.2
\( \vdash \psi \rightarrow \chi \)
mpsyl.3
\( \vdash \varphi \rightarrow \chi \rightarrow \theta \)
sylc l1 l2 _