Theorem sylancl

Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses
sylancl.1
\( \vdash \varphi \rightarrow \psi \)
sylancl.2
\( \vdash \chi \)
sylancl.3
\( \vdash \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \theta \)
Proof
l0
sylancl.1
\( \vdash \varphi \rightarrow \psi \)
sylancl.2
l2
a1i _
\( \vdash \varphi \rightarrow \chi \)
sylancl.3
\( \vdash \psi \wedge \chi \rightarrow \theta \)
syl2anc l0 l2 _