Theorem syl2an2

syl2an with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.)

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