Theorem syl2an

A double syllogism inference. For an implication-only version, see syl2im. (Contributed by NM, 31-Jan-1997.)

Hypotheses
syl2an.1
\( \vdash \varphi \rightarrow \psi \)
syl2an.2
\( \vdash \tau \rightarrow \chi \)
syl2an.3
\( \vdash \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \wedge \tau \rightarrow \theta \)
Proof
l0
syl2an.2
\( \vdash \tau \rightarrow \chi \)
l1
syl2an.1
\( \vdash \varphi \rightarrow \psi \)
syl2an.3
\( \vdash \psi \wedge \chi \rightarrow \theta \)
sylan l1 _
\( \vdash \varphi \wedge \chi \rightarrow \theta \)
sylan2 l0 _