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

Theorem exlimddv 1861
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 450 . . 3 (𝜑 → (𝜓𝜒))
43exlimdv 1859 . 2 (𝜑 → (∃𝑥𝜓𝜒))
51, 4mpd 15 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wex 1702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703
This theorem is referenced by:  fvmptdv2  6284  wfrlem17  7416  tfrlem9a  7467  erref  7747  domdifsn  8028  xpdom2  8040  enfixsn  8054  domunsn  8095  mapdom1  8110  sucdom2  8141  fineqvlem  8159  fissuni  8256  fipreima  8257  indexfi  8259  brwdom2  8463  wdomtr  8465  unwdomg  8474  unxpwdom  8479  infdifsn  8539  isinffi  8803  ac5num  8844  numacn  8857  acndom  8859  acndom2  8862  fodomacn  8864  infpss  9024  ssfin4  9117  domfin4  9118  enfin2i  9128  fin23lem31  9150  fin23lem41  9159  axcclem  9264  canthp1lem1  9459  canthp1  9461  winafp  9504  wun0  9525  prlem936  9854  supmul  10980  supxrre  12142  infxrre  12151  ixxub  12181  ixxlb  12182  relexpindlem  13784  isumltss  14561  eulerth  15469  ramub2  15699  mrieqv2d  16280  mreexexlem4d  16288  acsinfd  17161  acsdomd  17162  dfgrp3lem  17494  issubg2  17590  psgnunilem3  17897  sylow1lem4  17997  sylow3  18029  prmcyg  18276  ablfaclem3  18467  lbspss  19063  lsmcv  19122  cygzn  19900  lbslcic  20161  lmff  21086  tgcmp  21185  hauscmplem  21190  clsconn  21214  2ndcsep  21243  1stcelcls  21245  ptcnplem  21405  txcn  21410  fbdmn0  21619  ptcmplem2  21838  ptcmplem3  21839  tsmsxplem1  21937  met2ndci  22308  nmoid  22527  phtpcer  22775  phtpcerOLD  22776  phtpcco2  22780  cmetcau  23068  iscmet3lem2  23071  bcthlem4  23105  bcthlem5  23106  ovolicc2lem2  23267  vitali  23363  mbfimaopnlem  23403  limciun  23639  vieta1lem2  24047  tgldim0eq  25379  hpgerlem  25638  cusgrfi  26335  fusgrmaxsize  26341  minvecolem5  27707  foresf1o  29315  aciunf1lem  29435  fsumiunle  29549  locfinref  29882  esumcst  30099  esumiun  30130  unelldsys  30195  sigapildsys  30199  carsggect  30354  carsgclctunlem3  30356  erdsze2lem1  31159  erdsze2  31161  ptpconn  31189  cvmliftpht  31274  filnetlem3  32350  exlimimd  33161  poimirlem32  33412  mblfinlem2  33418  mblfinlem3  33419  mblfinlem4  33420  sdclem1  33510  sstotbnd  33545  prdsbnd  33563  prdstotbnd  33564  heibor1lem  33579  bfp  33594  llnn0  34621  lplnn0N  34652  lvoln0N  34696  diaglbN  36163  diaintclN  36166  dibglbN  36274  dibintclN  36275  dihglblem2aN  36401  dihintcl  36452  dvh1dim  36550  eldioph2lem1  37142  eldioph2lem2  37143  rencldnfilem  37203  kelac1  37452  hbt  37519  cncmpmax  39011  lptre2pt  39672  itgsubsticclem  39954  stoweidlem28  40008  stoweidlem31  40011  stoweidlem46  40026  stoweidlem53  40033  stoweidlem59  40039  setrec1  42203
  Copyright terms: Public domain W3C validator