Theorem 3ad2antl2

Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)

Hypothesis
3ad2antl.1
\( \vdash \varphi \wedge \chi \rightarrow \theta \)
Conclusion
\( \vdash (\psi \wedge \varphi \wedge \tau) \wedge \chi \rightarrow \theta \)
Proof
3ad2antl.1
adantlr _
3adantl1 _