Theorem syl2anc

Syllogism inference combined with contraction. (Contributed by NM, 16-Mar-2012.)

Hypotheses
syl2anc.1
\( \vdash \varphi \rightarrow \psi \)
syl2anc.2
\( \vdash \varphi \rightarrow \chi \)
syl2anc.3
\( \vdash \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \theta \)
Proof
l0
syl2anc.1
\( \vdash \varphi \rightarrow \psi \)
l1
syl2anc.2
\( \vdash \varphi \rightarrow \chi \)
syl2anc.3
ex _
\( \vdash \psi \rightarrow \chi \rightarrow \theta \)
sylc l0 l1 _