Theorem adantlll

Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 2-Dec-2012.)

Hypothesis
adantl2.1
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash \tau \wedge \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
Proof
l0
simpr
\( \vdash \tau \wedge \varphi \rightarrow \varphi \)
adantl2.1
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
sylanl1 l0 _