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

Theorem exlimddv 2014
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 397 . . 3 (𝜑 → (𝜓𝜒))
43exlimdv 2012 . 2 (𝜑 → (∃𝑥𝜓𝜒))
51, 4mpd 15 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wex 1851
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1852
This theorem is referenced by:  fvmptdv2  6440  wfrlem17  7583  tfrlem9a  7634  erref  7915  domdifsn  8198  xpdom2  8210  enfixsn  8224  domunsn  8265  mapdom1  8280  sucdom2  8311  fineqvlem  8329  fissuni  8426  fipreima  8427  indexfi  8429  brwdom2  8633  wdomtr  8635  unwdomg  8644  unxpwdom  8649  infdifsn  8717  isinffi  9017  ac5num  9058  numacn  9071  acndom  9073  acndom2  9076  fodomacn  9078  infpss  9240  ssfin4  9333  domfin4  9334  enfin2i  9344  fin23lem31  9366  fin23lem41  9375  axcclem  9480  canthp1lem1  9675  canthp1  9677  winafp  9720  wun0  9741  prlem936  10070  supmul  11196  supxrre  12361  infxrre  12370  ixxub  12400  ixxlb  12401  relexpindlem  14010  isumltss  14786  eulerth  15694  ramub2  15924  mrieqv2d  16506  mreexexlem4d  16514  acsinfd  17387  acsdomd  17388  dfgrp3lem  17720  issubg2  17816  psgnunilem3  18122  sylow1lem4  18222  sylow3  18254  prmcyg  18501  ablfaclem3  18693  lbspss  19294  lsmcv  19354  cygzn  20133  lbslcic  20396  lmff  21325  tgcmp  21424  hauscmplem  21429  clsconn  21453  2ndcsep  21482  1stcelcls  21484  ptcnplem  21644  txcn  21649  fbdmn0  21857  ptcmplem2  22076  ptcmplem3  22077  tsmsxplem1  22175  met2ndci  22546  nmoid  22765  phtpcer  23013  phtpcco2  23017  cmetcau  23305  iscmet3lem2  23308  bcthlem4  23342  bcthlem5  23343  ovolicc2lem2  23505  vitali  23600  mbfimaopnlem  23641  limciun  23877  vieta1lem2  24285  tgldim0eq  25618  hpgerlem  25877  cusgrfi  26588  fusgrmaxsize  26594  minvecolem5  28071  foresf1o  29675  aciunf1lem  29796  fsumiunle  29909  locfinref  30242  esumcst  30459  esumiun  30490  unelldsys  30555  sigapildsys  30559  carsggect  30714  carsgclctunlem3  30716  erdsze2lem1  31517  erdsze2  31519  ptpconn  31547  cvmliftpht  31632  filnetlem3  32706  exlimimd  33520  poimirlem32  33767  mblfinlem2  33773  mblfinlem3  33774  mblfinlem4  33775  sdclem1  33864  sstotbnd  33899  prdsbnd  33917  prdstotbnd  33918  heibor1lem  33933  bfp  33948  llnn0  35317  lplnn0N  35348  lvoln0N  35392  diaglbN  36858  diaintclN  36861  dibglbN  36969  dibintclN  36970  dihglblem2aN  37096  dihintcl  37147  dvh1dim  37245  eldioph2lem1  37842  eldioph2lem2  37843  rencldnfilem  37903  kelac1  38152  hbt  38219  cncmpmax  39707  lptre2pt  40384  itgsubsticclem  40702  stoweidlem28  40756  stoweidlem31  40759  stoweidlem46  40774  stoweidlem53  40781  stoweidlem59  40787  setrec1  42956
  Copyright terms: Public domain W3C validator