MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  im2anan9 Unicode version

Theorem im2anan9 831
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
StepHypRef Expression
1 im2an9.1 . . 3
21adantr 465 . 2
3 im2an9.2 . . 3
43adantl 466 . 2
52, 4anim12d 563 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  im2anan9r  832  ax12eq  2251  ax12el  2252  trin  4512  somo  4792  xpss12  5062  f1oun  5782  poxp  6818  soxp  6819  brecop  7327  ingru  9119  genpss  9310  genpnnp  9311  tgcl  18973  txlm  19620
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
  Copyright terms: Public domain W3C validator