MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exlimddv Structured version   Visualization version   GIF version

Theorem exlimddv 1850
Description: Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)
Hypotheses
Ref Expression
exlimddv.1 (𝜑 → ∃𝑥𝜓)
exlimddv.2 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
exlimddv (𝜑𝜒)
Distinct variable groups:   𝜒,𝑥   𝜑,𝑥
Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem exlimddv
StepHypRef Expression
1 exlimddv.1 . 2 (𝜑 → ∃𝑥𝜓)
2 exlimddv.2 . . . 4 ((𝜑𝜓) → 𝜒)
32ex 449 . . 3 (𝜑 → (𝜓𝜒))
43exlimdv 1848 . 2 (𝜑 → (∃𝑥𝜓𝜒))
51, 4mpd 15 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wex 1695
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827
This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696
This theorem is referenced by:  fvmptdv2  6206  wfrlem17  7318  tfrlem9a  7369  erref  7649  domdifsn  7928  xpdom2  7940  enfixsn  7954  domunsn  7995  mapdom1  8010  sucdom2  8041  fineqvlem  8059  fissuni  8154  fipreima  8155  indexfi  8157  brwdom2  8361  wdomtr  8363  unwdomg  8372  unxpwdom  8377  infdifsn  8437  isinffi  8701  ac5num  8742  numacn  8755  acndom  8757  acndom2  8760  fodomacn  8762  infpss  8922  ssfin4  9015  domfin4  9016  enfin2i  9026  fin23lem31  9048  fin23lem41  9057  axcclem  9162  canthp1lem1  9353  canthp1  9355  winafp  9398  wun0  9419  prlem936  9748  supmul  10872  supxrre  12029  infxrre  12038  ixxub  12067  ixxlb  12068  relexpindlem  13651  isumltss  14419  eulerth  15326  ramub2  15556  mrieqv2d  16122  mreexexlem4d  16130  acsinfd  17003  acsdomd  17004  dfgrp3lem  17336  issubg2  17432  psgnunilem3  17739  sylow1lem4  17839  sylow3  17871  prmcyg  18118  ablfaclem3  18309  lbspss  18903  lsmcv  18962  cygzn  19738  lbslcic  19999  lmff  20915  tgcmp  21014  hauscmplem  21019  clscon  21043  2ndcsep  21072  1stcelcls  21074  ptcnplem  21234  txcn  21239  fbdmn0  21448  ptcmplem2  21667  ptcmplem3  21668  tsmsxplem1  21766  met2ndci  22137  nmoid  22356  phtpcer  22602  phtpcerOLD  22603  phtpcco2  22607  cmetcau  22895  iscmet3lem2  22898  bcthlem4  22932  bcthlem5  22933  ovolicc2lem2  23093  vitali  23188  mbfimaopnlem  23228  limciun  23464  vieta1lem2  23870  tgldim0eq  25198  hpgerlem  25457  cusgrafi  26010  usgramaxsize  26015  minvecolem5  27121  foresf1o  28727  aciunf1lem  28844  locfinref  29236  esumcst  29452  esumiun  29483  unelldsys  29548  sigapildsys  29552  carsggect  29707  carsgclctunlem3  29709  erdsze2lem1  30439  erdsze2  30441  ptpcon  30469  cvmliftpht  30554  filnetlem3  31545  exlimimd  32366  poimirlem32  32611  mblfinlem2  32617  mblfinlem3  32618  mblfinlem4  32619  sdclem1  32709  sstotbnd  32744  prdsbnd  32762  prdstotbnd  32763  heibor1lem  32778  bfp  32793  llnn0  33820  lplnn0N  33851  lvoln0N  33895  diaglbN  35362  diaintclN  35365  dibglbN  35473  dibintclN  35474  dihglblem2aN  35600  dihintcl  35651  dvh1dim  35749  eldioph2lem1  36341  eldioph2lem2  36342  rencldnfilem  36402  kelac1  36651  hbt  36719  cncmpmax  38214  lptre2pt  38707  itgsubsticclem  38867  stoweidlem28  38921  stoweidlem31  38924  stoweidlem46  38939  stoweidlem53  38946  stoweidlem59  38952  cusgrfi  40674  fusgrmaxsize  40680  setrec1  42237
  Copyright terms: Public domain W3C validator