Theorem syl2an23an

Deduction related to syl3an with antecedents in standard conjunction form. (Contributed by Alan Sare, 31-Aug-2016.) (Proof shortened by Wolf Lammen, 28-Jun-2022.)

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