Theorem anim12dan

Conjoin antecedents and consequents in a deduction. (Contributed by Jeff Madsen, 16-Jun-2011.)

Hypotheses
anim12dan.1
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
anim12dan.2
\( \vdash \varphi \wedge \theta \rightarrow \tau \)
Conclusion
\( \vdash \varphi \wedge (\psi \wedge \theta) \rightarrow \chi \wedge \tau \)
Proof
anim12dan.1
l1
ex _
anim12dan.2
ex _
anim12d l1 _
imp _