Theorem mpsylsyld

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

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