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

Theorem exlimddv 1903
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 1901 . 2 (𝜑 → (∃𝑥𝜓𝜒))
51, 4mpd 15 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wex 1744
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745
This theorem is referenced by:  fvmptdv2  6337  wfrlem17  7476  tfrlem9a  7527  erref  7807  domdifsn  8084  xpdom2  8096  enfixsn  8110  domunsn  8151  mapdom1  8166  sucdom2  8197  fineqvlem  8215  fissuni  8312  fipreima  8313  indexfi  8315  brwdom2  8519  wdomtr  8521  unwdomg  8530  unxpwdom  8535  infdifsn  8592  isinffi  8856  ac5num  8897  numacn  8910  acndom  8912  acndom2  8915  fodomacn  8917  infpss  9077  ssfin4  9170  domfin4  9171  enfin2i  9181  fin23lem31  9203  fin23lem41  9212  axcclem  9317  canthp1lem1  9512  canthp1  9514  winafp  9557  wun0  9578  prlem936  9907  supmul  11033  supxrre  12195  infxrre  12204  ixxub  12234  ixxlb  12235  relexpindlem  13847  isumltss  14624  eulerth  15535  ramub2  15765  mrieqv2d  16346  mreexexlem4d  16354  acsinfd  17227  acsdomd  17228  dfgrp3lem  17560  issubg2  17656  psgnunilem3  17962  sylow1lem4  18062  sylow3  18094  prmcyg  18341  ablfaclem3  18532  lbspss  19130  lsmcv  19189  cygzn  19967  lbslcic  20228  lmff  21153  tgcmp  21252  hauscmplem  21257  clsconn  21281  2ndcsep  21310  1stcelcls  21312  ptcnplem  21472  txcn  21477  fbdmn0  21685  ptcmplem2  21904  ptcmplem3  21905  tsmsxplem1  22003  met2ndci  22374  nmoid  22593  phtpcer  22841  phtpcco2  22845  cmetcau  23133  iscmet3lem2  23136  bcthlem4  23170  bcthlem5  23171  ovolicc2lem2  23332  vitali  23427  mbfimaopnlem  23467  limciun  23703  vieta1lem2  24111  tgldim0eq  25443  hpgerlem  25702  cusgrfi  26410  fusgrmaxsize  26416  minvecolem5  27865  foresf1o  29469  aciunf1lem  29590  fsumiunle  29703  locfinref  30036  esumcst  30253  esumiun  30284  unelldsys  30349  sigapildsys  30353  carsggect  30508  carsgclctunlem3  30510  erdsze2lem1  31311  erdsze2  31313  ptpconn  31341  cvmliftpht  31426  filnetlem3  32500  exlimimd  33320  poimirlem32  33571  mblfinlem2  33577  mblfinlem3  33578  mblfinlem4  33579  sdclem1  33669  sstotbnd  33704  prdsbnd  33722  prdstotbnd  33723  heibor1lem  33738  bfp  33753  llnn0  35120  lplnn0N  35151  lvoln0N  35195  diaglbN  36661  diaintclN  36664  dibglbN  36772  dibintclN  36773  dihglblem2aN  36899  dihintcl  36950  dvh1dim  37048  eldioph2lem1  37640  eldioph2lem2  37641  rencldnfilem  37701  kelac1  37950  hbt  38017  cncmpmax  39505  lptre2pt  40190  itgsubsticclem  40509  stoweidlem28  40563  stoweidlem31  40566  stoweidlem46  40581  stoweidlem53  40588  stoweidlem59  40594  setrec1  42763
  Copyright terms: Public domain W3C validator