Theorem syld3an2

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

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