Theorem anim12ii

Conjoin antecedents and consequents in a deduction. (Contributed by NM, 11-Nov-2007.) (Proof shortened by Wolf Lammen, 19-Jul-2013.)

Hypotheses
anim12ii.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
anim12ii.2
\( \vdash \theta \rightarrow \psi \rightarrow \tau \)
Conclusion
\( \vdash \varphi \wedge \theta \rightarrow \psi \rightarrow \chi \wedge \tau \)
Proof
l0
anim12ii.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
l1
anim12ii.2
\( \vdash \theta \rightarrow \psi \rightarrow \tau \)
pm3.43
\( \vdash (\psi \rightarrow \chi) \wedge (\psi \rightarrow \tau) \rightarrow \psi \rightarrow \chi \wedge \tau \)
syl2an l0 l1 _