Theorem im2anan9r

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 \theta \wedge \varphi \rightarrow \psi \wedge \tau \rightarrow \chi \wedge \eta \)
Proof
l0
im2an9.1
im2an9.2
im2anan9 l0 _
ancoms _