Theorem im2anan9

Deduction joining nested implications to form implication of conjunctions. (Contributed by NM, 29-Feb-1996.)

Hypotheses
im2an9.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
im2an9.2
\( \vdash \theta \rightarrow \tau \rightarrow \eta \)
Conclusion
\( \vdash \varphi \wedge \theta \rightarrow \psi \wedge \tau \rightarrow \chi \wedge \eta \)
Proof
im2an9.1
l1
adantrd _
im2an9.2
adantld _
anim12ii l1 _