Theorem syl2an2r

syl2anr with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.) (Proof shortened by Wolf Lammen, 28-Mar-2022.)

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