Theorem syld3an1

A syllogism inference. (Contributed by NM, 7-Jul-2008.) (Proof shortened by Wolf Lammen, 26-Jun-2022.)

Hypotheses
syld3an1.1
\( \vdash \chi \wedge \psi \wedge \theta \rightarrow \varphi \)
syld3an1.2
\( \vdash \varphi \wedge \psi \wedge \theta \rightarrow \tau \)
Conclusion
\( \vdash \chi \wedge \psi \wedge \theta \rightarrow \tau \)
Proof
l0
syld3an1.1
\( \vdash \chi \wedge \psi \wedge \theta \rightarrow \varphi \)
l1
simp2
\( \vdash \chi \wedge \psi \wedge \theta \rightarrow \psi \)
l2
simp3
\( \vdash \chi \wedge \psi \wedge \theta \rightarrow \theta \)
syld3an1.2
\( \vdash \varphi \wedge \psi \wedge \theta \rightarrow \tau \)
syl3anc l0 l1 l2 _