Theorem sylc

A syllogism inference combined with contraction. (Contributed by NM, 4-May-1994.) (Revised by NM, 13-Jul-2013.)

Hypotheses
sylc.1
\( \vdash \varphi \rightarrow \psi \)
sylc.2
\( \vdash \varphi \rightarrow \chi \)
sylc.3
\( \vdash \psi \rightarrow \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \theta \)
Proof
l0
sylc.1
\( \vdash \varphi \rightarrow \psi \)
l1
sylc.2
\( \vdash \varphi \rightarrow \chi \)
sylc.3
\( \vdash \psi \rightarrow \chi \rightarrow \theta \)
syl2im l0 l1 _
pm2.43i _