Theorem mpisyl

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

Hypotheses
mpisyl.1
\( \vdash \varphi \rightarrow \psi \)
mpisyl.2
\( \vdash \chi \)
mpisyl.3
\( \vdash \psi \rightarrow \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \theta \)
Proof
l0
mpisyl.1
\( \vdash \varphi \rightarrow \psi \)
l1
mpisyl.2
\( \vdash \chi \)
mpisyl.3
\( \vdash \psi \rightarrow \chi \rightarrow \theta \)
mpi l1 _
\( \vdash \psi \rightarrow \theta \)
syl l0 _