Theorem syl3an132

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

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