Theorem syld3an3

A syllogism inference. (Contributed by NM, 20-May-2007.)

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