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

Theorem exlimddv 1731
Description: Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)
Hypotheses
Ref Expression
exlimddv.1  |-  ( ph  ->  E. x ps )
exlimddv.2  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
exlimddv  |-  ( ph  ->  ch )
Distinct variable groups:    ch, x    ph, x
Allowed substitution hint:    ps( x)

Proof of Theorem exlimddv
StepHypRef Expression
1 exlimddv.1 . 2  |-  ( ph  ->  E. x ps )
2 exlimddv.2 . . . 4  |-  ( (
ph  /\  ps )  ->  ch )
32ex 432 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
43exlimdv 1729 . 2  |-  ( ph  ->  ( E. x ps 
->  ch ) )
51, 4mpd 15 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367   E.wex 1617
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618
This theorem is referenced by:  fvmptdv2  5945  tfrlem9a  7047  erref  7323  domdifsn  7593  xpdom2  7605  enfixsn  7619  domunsn  7660  mapdom1  7675  sucdom2  7707  fineqvlem  7727  fissuni  7817  fipreima  7818  indexfi  7820  brwdom2  7991  wdomtr  7993  unwdomg  8002  unxpwdom  8007  infdifsn  8064  isinffi  8364  ac5num  8408  numacn  8421  acndom  8423  acndom2  8426  fodomacn  8428  infpss  8588  ssfin4  8681  domfin4  8682  enfin2i  8692  fin23lem31  8714  fin23lem41  8723  axcclem  8828  canthp1lem1  9019  canthp1  9021  winafp  9064  wun0  9085  prlem936  9414  supmul  10506  supxrre  11522  infmxrre  11530  ixxub  11553  ixxlb  11554  relexpindlem  12978  isumltss  13742  eulerth  14397  ramub2  14616  mrieqv2d  15128  mreexexlem4d  15136  acsinfd  16009  acsdomd  16010  issubg2  16415  psgnunilem3  16720  sylow1lem4  16820  sylow3  16852  prmcyg  17095  ablfaclem3  17333  lbspss  17923  lsmcv  17982  cygzn  18782  lbslcic  19043  lmff  19969  tgcmp  20068  hauscmplem  20073  clscon  20097  2ndcsep  20126  1stcelcls  20128  ptcnplem  20288  txcn  20293  fbdmn0  20501  ptcmplem2  20719  ptcmplem3  20720  tsmsxplem1  20821  met2ndci  21191  nmoid  21415  phtpcer  21661  phtpcco2  21665  cmetcau  21894  iscmet3lem2  21897  bcthlem4  21932  bcthlem5  21933  ovolicc2lem2  22095  vitali  22188  mbfimaopnlem  22228  limciun  22464  vieta1lem2  22873  tgldim0eq  24095  hpgerlem  24335  cusgrafi  24684  usgramaxsize  24689  isgrp2d  25435  minvecolem5  25995  foresf1o  27602  aciunf1lem  27729  locfinref  28079  esumcst  28292  esumiun  28323  sigapildsys  28388  carsggect  28526  carsgclctunlem3  28528  erdsze2lem1  28911  erdsze2  28913  ptpcon  28942  cvmliftpht  29027  mblfinlem2  30292  mblfinlem3  30293  mblfinlem4  30294  filnetlem3  30438  sdclem1  30476  sstotbnd  30511  prdsbnd  30529  prdstotbnd  30530  heibor1lem  30545  bfp  30560  eldioph2lem1  30932  eldioph2lem2  30933  rencldnfilem  30993  kelac1  31248  hbt  31320  cncmpmax  31647  lptre2pt  31885  itgsubsticclem  32013  stoweidlem28  32049  stoweidlem31  32052  stoweidlem46  32067  stoweidlem53  32074  stoweidlem59  32080  llnn0  35637  lplnn0N  35668  lvoln0N  35712  diaglbN  37179  diaintclN  37182  dibglbN  37290  dibintclN  37291  dihglblem2aN  37417  dihintcl  37468  dvh1dim  37566
  Copyright terms: Public domain W3C validator