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

Theorem exlimddv 1927
Description: Existential elimination rule of natural deduction (Rule C, explained in exlimiv 1922). (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 1925 . 2 (𝜑 → (∃𝑥𝜓𝜒))
51, 4mpd 15 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wex 1771
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772
This theorem is referenced by:  fvmptdv2  6778  wfrlem17  7960  tfrlem9a  8011  erref  8298  domdifsn  8588  xpdom2  8600  enfixsn  8614  domunsn  8655  mapdom1  8670  sucdom2  8702  fineqvlem  8720  fissuni  8817  fipreima  8818  indexfi  8820  brwdom2  9025  wdomtr  9027  unwdomg  9036  unxpwdom  9041  infdifsn  9108  isinffi  9409  ac5num  9450  numacn  9463  acndom  9465  acndom2  9468  fodomacn  9470  infpss  9627  ssfin4  9720  domfin4  9721  enfin2i  9731  fin23lem31  9753  fin23lem41  9762  axcclem  9867  canthp1lem1  10062  canthp1  10064  winafp  10107  wun0  10128  prlem936  10457  supmul  11601  supxrre  12708  infxrre  12717  ixxub  12747  ixxlb  12748  hash1elsn  13720  relexpindlem  14410  isumltss  15191  eulerth  16108  ramub2  16338  mrieqv2d  16898  mreexexlem4d  16906  acsinfd  17778  acsdomd  17779  dfgrp3lem  18135  issubg2  18232  psgnunilem3  18553  sylow1lem4  18655  sylow3  18687  prmcyg  18943  ablfaclem3  19138  lbspss  19783  lsmcv  19842  cygzn  20645  lbslcic  20913  lmff  21837  tgcmp  21937  hauscmplem  21942  clsconn  21966  2ndcsep  21995  1stcelcls  21997  ptcnplem  22157  txcn  22162  fbdmn0  22370  ptcmplem2  22589  ptcmplem3  22590  tsmsxplem1  22688  met2ndci  23059  nmoid  23278  phtpcer  23526  phtpcco2  23530  cmetcau  23819  iscmet3lem2  23822  bcthlem4  23857  bcthlem5  23858  ovolicc2lem2  24046  vitali  24141  mbfimaopnlem  24183  limciun  24419  vieta1lem2  24827  tgldim0eq  26216  hpgerlem  26478  cusgrfi  27167  fusgrmaxsize  27173  minvecolem5  28585  foresf1o  30192  unidifsnel  30222  unidifsnne  30223  aciunf1lem  30335  fsumiunle  30472  cycpmconjslem2  30724  cycpmconjs  30725  dimcl  30902  lvecdim0i  30903  lvecdim0  30904  lssdimle  30905  dimpropd  30906  dimkerim  30922  fedgmul  30926  extdg1id  30952  locfinref  31004  esumcst  31221  esumiun  31252  unelldsys  31316  sigapildsys  31320  carsggect  31475  carsgclctunlem3  31477  erdsze2lem1  32347  erdsze2  32349  ptpconn  32377  cvmliftpht  32462  filnetlem3  33625  exlimimd  34506  poimirlem32  34805  mblfinlem2  34811  mblfinlem3  34812  mblfinlem4  34813  sdclem1  34899  sstotbnd  34934  prdsbnd  34952  prdstotbnd  34953  heibor1lem  34968  bfp  34983  eqvrelref  35725  llnn0  36532  lplnn0N  36563  lvoln0N  36607  diaglbN  38071  diaintclN  38074  dibglbN  38182  dibintclN  38183  dihglblem2aN  38309  dihintcl  38360  dvh1dim  38458  eldioph2lem1  39235  eldioph2lem2  39236  rencldnfilem  39295  kelac1  39541  hbt  39608  cpcoll2d  40472  cncmpmax  41166  lptre2pt  41797  itgsubsticclem  42136  stoweidlem28  42190  stoweidlem31  42193  stoweidlem46  42208  stoweidlem53  42215  stoweidlem59  42221  uniimaelsetpreimafv  43433  setrec1  44722
  Copyright terms: Public domain W3C validator