Theorem syl2an3an

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

Hypotheses
syl2an3an.1
\( \vdash \varphi \rightarrow \psi \)
syl2an3an.2
\( \vdash \varphi \rightarrow \chi \)
syl2an3an.3
\( \vdash \theta \rightarrow \tau \)
syl2an3an.4
\( \vdash \psi \wedge \chi \wedge \tau \rightarrow \eta \)
Conclusion
\( \vdash \varphi \wedge \theta \rightarrow \eta \)
Proof
l0
syl2an3an.1
\( \vdash \varphi \rightarrow \psi \)
l1
syl2an3an.2
\( \vdash \varphi \rightarrow \chi \)
l2
syl2an3an.3
\( \vdash \theta \rightarrow \tau \)
syl2an3an.4
\( \vdash \psi \wedge \chi \wedge \tau \rightarrow \eta \)
syl3an l0 l1 l2 _
3anidm12 _