Theorem ad2ant2l

Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)

Hypothesis
ad2ant2.1
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
Conclusion
\( \vdash \theta \wedge \varphi \wedge (\tau \wedge \psi) \rightarrow \chi \)
Proof
ad2ant2.1
adantrl _
adantll _