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

Theorem exlimddv 1774
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 435 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
43exlimdv 1772 . 2  |-  ( ph  ->  ( E. x ps 
->  ch ) )
51, 4mpd 15 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370   E.wex 1657
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1658
This theorem is referenced by:  fvmptdv2  5918  wfrlem17  7002  tfrlem9a  7054  erref  7333  domdifsn  7603  xpdom2  7615  enfixsn  7629  domunsn  7670  mapdom1  7685  sucdom2  7716  fineqvlem  7734  fissuni  7827  fipreima  7828  indexfi  7830  brwdom2  8036  wdomtr  8038  unwdomg  8047  unxpwdom  8052  infdifsn  8109  isinffi  8373  ac5num  8413  numacn  8426  acndom  8428  acndom2  8431  fodomacn  8433  infpss  8593  ssfin4  8686  domfin4  8687  enfin2i  8697  fin23lem31  8719  fin23lem41  8728  axcclem  8833  canthp1lem1  9023  canthp1  9025  winafp  9068  wun0  9089  prlem936  9418  supmul  10525  supxrre  11559  infxrre  11568  infmxrreOLD  11572  ixxub  11602  ixxlb  11603  ixxlbOLD  11604  relexpindlem  13065  isumltss  13844  eulerth  14669  ramub2  14909  mrieqv2d  15483  mreexexlem4d  15491  acsinfd  16364  acsdomd  16365  issubg2  16770  psgnunilem3  17075  sylow1lem4  17191  sylow3  17223  prmcyg  17466  ablfaclem3  17658  lbspss  18243  lsmcv  18302  cygzn  19078  lbslcic  19336  lmff  20254  tgcmp  20353  hauscmplem  20358  clscon  20382  2ndcsep  20411  1stcelcls  20413  ptcnplem  20573  txcn  20578  fbdmn0  20786  ptcmplem2  21005  ptcmplem3  21006  tsmsxplem1  21104  met2ndci  21474  nmoid  21700  phtpcer  21963  phtpcco2  21967  cmetcau  22196  iscmet3lem2  22199  bcthlem4  22232  bcthlem5  22233  ovolicc2lem2  22408  vitali  22508  mbfimaopnlem  22548  limciun  22786  vieta1lem2  23201  tgldim0eq  24484  hpgerlem  24744  cusgrafi  25147  usgramaxsize  25152  isgrp2d  25900  minvecolem5  26460  minvecolem5OLD  26470  foresf1o  28077  aciunf1lem  28205  locfinref  28615  esumcst  28831  esumiun  28862  unelldsys  28927  sigapildsys  28931  carsggect  29097  carsgclctunlem3  29099  erdsze2lem1  29873  erdsze2  29875  ptpcon  29903  cvmliftpht  29988  filnetlem3  30980  exlimimd  31652  poimirlem32  31879  mblfinlem2  31885  mblfinlem3  31886  mblfinlem4  31887  sdclem1  31979  sstotbnd  32014  prdsbnd  32032  prdstotbnd  32033  heibor1lem  32048  bfp  32063  llnn0  32993  lplnn0N  33024  lvoln0N  33068  diaglbN  34535  diaintclN  34538  dibglbN  34646  dibintclN  34647  dihglblem2aN  34773  dihintcl  34824  dvh1dim  34922  eldioph2lem1  35514  eldioph2lem2  35515  rencldnfilem  35575  kelac1  35834  hbt  35902  cncmpmax  37269  lptre2pt  37603  itgsubsticclem  37735  stoweidlem28  37771  stoweidlem31  37775  stoweidlem46  37790  stoweidlem53  37797  stoweidlem59  37803  cusgrfi  39247  fusgrmaxsize  39253
  Copyright terms: Public domain W3C validator