Theorem im2anan9 835

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

Hypotheses

Ref	Expression
im2an9.1
im2an9.2

Assertion

Ref	Expression
im2anan9

Proof of Theorem im2anan9

Step	Hyp	Ref	Expression
1		im2an9.1	. . 3
2	1	adantr 465	. 2
3		im2an9.2	. . 3
4	3	adantl 466	. 2
5	2, 4	anim12d 563	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  im2anan9r  836  ax12eq  2271  ax12el  2272  trin  4555  somo  4839  xpss12  5113  f1oun  5840  poxp  6912  soxp  6913  brecop  7423  ingru  9214  genpss  9403  genpnnp  9404  tgcl  19471  txlm  20149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-an 371