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

Theorem exlimddv 1849
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 448 . . 3 (𝜑 → (𝜓𝜒))
43exlimdv 1847 . 2 (𝜑 → (∃𝑥𝜓𝜒))
51, 4mpd 15 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wex 1694
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695
This theorem is referenced by:  fvmptdv2  6190  wfrlem17  7295  tfrlem9a  7346  erref  7626  domdifsn  7905  xpdom2  7917  enfixsn  7931  domunsn  7972  mapdom1  7987  sucdom2  8018  fineqvlem  8036  fissuni  8131  fipreima  8132  indexfi  8134  brwdom2  8338  wdomtr  8340  unwdomg  8349  unxpwdom  8354  infdifsn  8414  isinffi  8678  ac5num  8719  numacn  8732  acndom  8734  acndom2  8737  fodomacn  8739  infpss  8899  ssfin4  8992  domfin4  8993  enfin2i  9003  fin23lem31  9025  fin23lem41  9034  axcclem  9139  canthp1lem1  9330  canthp1  9332  winafp  9375  wun0  9396  prlem936  9725  supmul  10844  supxrre  11987  infxrre  11996  ixxub  12025  ixxlb  12026  relexpindlem  13599  isumltss  14367  eulerth  15274  ramub2  15504  mrieqv2d  16070  mreexexlem4d  16078  acsinfd  16951  acsdomd  16952  dfgrp3lem  17284  issubg2  17380  psgnunilem3  17687  sylow1lem4  17787  sylow3  17819  prmcyg  18066  ablfaclem3  18257  lbspss  18851  lsmcv  18910  cygzn  19685  lbslcic  19946  lmff  20862  tgcmp  20961  hauscmplem  20966  clscon  20990  2ndcsep  21019  1stcelcls  21021  ptcnplem  21181  txcn  21186  fbdmn0  21395  ptcmplem2  21614  ptcmplem3  21615  tsmsxplem1  21713  met2ndci  22084  nmoid  22303  phtpcer  22549  phtpcerOLD  22550  phtpcco2  22554  cmetcau  22839  iscmet3lem2  22842  bcthlem4  22876  bcthlem5  22877  ovolicc2lem2  23037  vitali  23132  mbfimaopnlem  23172  limciun  23408  vieta1lem2  23814  tgldim0eq  25142  hpgerlem  25402  cusgrafi  25803  usgramaxsize  25808  minvecolem5  26914  foresf1o  28520  aciunf1lem  28637  locfinref  29029  esumcst  29245  esumiun  29276  unelldsys  29341  sigapildsys  29345  carsggect  29500  carsgclctunlem3  29502  erdsze2lem1  30232  erdsze2  30234  ptpcon  30262  cvmliftpht  30347  filnetlem3  31338  exlimimd  32149  poimirlem32  32394  mblfinlem2  32400  mblfinlem3  32401  mblfinlem4  32402  sdclem1  32492  sstotbnd  32527  prdsbnd  32545  prdstotbnd  32546  heibor1lem  32561  bfp  32576  llnn0  33603  lplnn0N  33634  lvoln0N  33678  diaglbN  35145  diaintclN  35148  dibglbN  35256  dibintclN  35257  dihglblem2aN  35383  dihintcl  35434  dvh1dim  35532  eldioph2lem1  36124  eldioph2lem2  36125  rencldnfilem  36185  kelac1  36434  hbt  36502  cncmpmax  37997  lptre2pt  38490  itgsubsticclem  38650  stoweidlem28  38704  stoweidlem31  38707  stoweidlem46  38722  stoweidlem53  38729  stoweidlem59  38735  cusgrfi  40655  fusgrmaxsize  40661
  Copyright terms: Public domain W3C validator