Theorem anim12i

Conjoin antecedents and consequents of two premises. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 14-Dec-2013.)

Hypotheses
anim12i.1
\( \vdash \varphi \rightarrow \psi \)
anim12i.2
\( \vdash \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \wedge \chi \rightarrow \psi \wedge \theta \)
Proof
l0
anim12i.1
\( \vdash \varphi \rightarrow \psi \)
l1
anim12i.2
\( \vdash \chi \rightarrow \theta \)
id
\( \vdash \psi \wedge \theta \rightarrow \psi \wedge \theta \)
syl2an l0 l1 _