Theorem syl2anc2

Double syllogism inference combined with contraction. (Contributed by BTernaryTau, 29-Sep-2023.)

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