Theorem sylancr

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

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