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

Theorem exlimddv 1929
Description: Existential elimination rule of natural deduction (Rule C, explained in exlimiv 1924). (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 413 . . 3 (𝜑 → (𝜓𝜒))
43exlimdv 1927 . 2 (𝜑 → (∃𝑥𝜓𝜒))
51, 4mpd 15 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wex 1773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774
This theorem is referenced by:  fvmptdv2  6782  wfrlem17  7962  tfrlem9a  8013  erref  8299  domdifsn  8589  xpdom2  8601  enfixsn  8615  domunsn  8656  mapdom1  8671  sucdom2  8703  fineqvlem  8721  fissuni  8818  fipreima  8819  indexfi  8821  brwdom2  9026  wdomtr  9028  unwdomg  9037  unxpwdom  9042  infdifsn  9109  isinffi  9410  ac5num  9451  numacn  9464  acndom  9466  acndom2  9469  fodomacn  9471  infpss  9628  ssfin4  9721  domfin4  9722  enfin2i  9732  fin23lem31  9754  fin23lem41  9763  axcclem  9868  canthp1lem1  10063  canthp1  10065  winafp  10108  wun0  10129  prlem936  10458  supmul  11602  supxrre  12710  infxrre  12719  ixxub  12749  ixxlb  12750  hash1elsn  13722  relexpindlem  14412  isumltss  15193  eulerth  16110  ramub2  16340  mrieqv2d  16900  mreexexlem4d  16908  acsinfd  17780  acsdomd  17781  dfgrp3lem  18127  issubg2  18224  psgnunilem3  18544  sylow1lem4  18646  sylow3  18678  prmcyg  18934  ablfaclem3  19129  lbspss  19774  lsmcv  19833  cygzn  20633  lbslcic  20901  lmff  21825  tgcmp  21925  hauscmplem  21930  clsconn  21954  2ndcsep  21983  1stcelcls  21985  ptcnplem  22145  txcn  22150  fbdmn0  22358  ptcmplem2  22577  ptcmplem3  22578  tsmsxplem1  22676  met2ndci  23047  nmoid  23266  phtpcer  23514  phtpcco2  23518  cmetcau  23807  iscmet3lem2  23810  bcthlem4  23845  bcthlem5  23846  ovolicc2lem2  24034  vitali  24129  mbfimaopnlem  24171  limciun  24407  vieta1lem2  24815  tgldim0eq  26203  hpgerlem  26465  cusgrfi  27154  fusgrmaxsize  27160  minvecolem5  28572  foresf1o  30179  unidifsnel  30209  unidifsnne  30210  aciunf1lem  30322  fsumiunle  30459  cycpmconjslem2  30711  cycpmconjs  30712  dimcl  30889  lvecdim0i  30890  lvecdim0  30891  lssdimle  30892  dimpropd  30893  dimkerim  30909  fedgmul  30913  extdg1id  30939  locfinref  30991  esumcst  31208  esumiun  31239  unelldsys  31303  sigapildsys  31307  carsggect  31462  carsgclctunlem3  31464  erdsze2lem1  32334  erdsze2  32336  ptpconn  32364  cvmliftpht  32449  filnetlem3  33612  exlimimd  34493  poimirlem32  34791  mblfinlem2  34797  mblfinlem3  34798  mblfinlem4  34799  sdclem1  34886  sstotbnd  34921  prdsbnd  34939  prdstotbnd  34940  heibor1lem  34955  bfp  34970  eqvrelref  35712  llnn0  36519  lplnn0N  36550  lvoln0N  36594  diaglbN  38058  diaintclN  38061  dibglbN  38169  dibintclN  38170  dihglblem2aN  38296  dihintcl  38347  dvh1dim  38445  eldioph2lem1  39222  eldioph2lem2  39223  rencldnfilem  39282  kelac1  39528  hbt  39595  cpcoll2d  40460  cncmpmax  41154  lptre2pt  41786  itgsubsticclem  42125  stoweidlem28  42179  stoweidlem31  42182  stoweidlem46  42197  stoweidlem53  42204  stoweidlem59  42210  setrec1  44626
  Copyright terms: Public domain W3C validator