Theorem anim12d

Conjoin antecedents and consequents in a deduction. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 18-Dec-2013.)

Hypotheses
anim12d.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
anim12d.2
\( \vdash \varphi \rightarrow \theta \rightarrow \tau \)
Conclusion
\( \vdash \varphi \rightarrow \psi \wedge \theta \rightarrow \chi \wedge \tau \)
Proof
l0
anim12d.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
l1
anim12d.2
\( \vdash \varphi \rightarrow \theta \rightarrow \tau \)
idd
\( \vdash \varphi \rightarrow \chi \wedge \tau \rightarrow \chi \wedge \tau \)
syl2and l0 l1 _