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

Theorem exlimddv 1692
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 434 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
43exlimdv 1690 . 2  |-  ( ph  ->  ( E. x ps 
->  ch ) )
51, 4mpd 15 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   E.wex 1586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587
This theorem is referenced by:  fvmptdv2  5802  tfrlem9a  6860  erref  7136  domdifsn  7409  xpdom2  7421  enfixsn  7435  domunsn  7476  mapdom1  7491  sucdom2  7522  fineqvlem  7542  fissuni  7631  fipreima  7632  indexfi  7634  brwdom2  7803  wdomtr  7805  unwdomg  7814  unxpwdom  7819  infdifsn  7877  isinffi  8177  ac5num  8221  numacn  8234  acndom  8236  acndom2  8239  fodomacn  8241  infpss  8401  ssfin4  8494  domfin4  8495  enfin2i  8505  fin23lem31  8527  fin23lem41  8536  axcclem  8641  canthp1lem1  8834  canthp1  8836  winafp  8879  wun0  8900  prlem936  9231  supmul  10313  supxrre  11305  infmxrre  11313  ixxub  11336  ixxlb  11337  isumltss  13326  eulerth  13873  ramub2  14090  mrieqv2d  14592  mreexexlem4d  14600  acsinfd  15365  acsdomd  15366  issubg2  15711  psgnunilem3  16017  sylow1lem4  16115  sylow3  16147  prmcyg  16385  ablfaclem3  16603  lbspss  17178  lsmcv  17237  cygzn  18018  lbslcic  18285  lmff  18920  tgcmp  19019  hauscmplem  19024  clscon  19049  2ndcsep  19078  1stcelcls  19080  ptcnplem  19209  txcn  19214  fbdmn0  19422  ptcmplem2  19640  ptcmplem3  19641  tsmsxplem1  19742  met2ndci  20112  nmoid  20336  phtpcer  20582  phtpcco2  20586  cmetcau  20815  iscmet3lem2  20818  bcthlem4  20853  bcthlem5  20854  ovolicc2lem2  21016  vitali  21108  mbfimaopnlem  21148  limciun  21384  vieta1lem2  21792  cusgrafi  23405  usgramaxsize  23410  isgrp2d  23737  minvecolem5  24297  esumcst  26529  erdsze2lem1  27106  erdsze2  27108  ptpcon  27137  cvmliftpht  27222  relexpindlem  27356  mblfinlem2  28448  mblfinlem3  28449  mblfinlem4  28450  filnetlem3  28620  sdclem1  28658  sstotbnd  28693  prdsbnd  28711  prdstotbnd  28712  heibor1lem  28727  bfp  28742  eldioph2lem1  29117  eldioph2lem2  29118  rencldnfilem  29178  kelac1  29435  hbt  29505  cncmpmax  29773  stoweidlem28  29842  stoweidlem31  29845  stoweidlem46  29860  stoweidlem53  29867  stoweidlem59  29873  llnn0  33179  lplnn0N  33210  lvoln0N  33254  diaglbN  34719  diaintclN  34722  dibglbN  34830  dibintclN  34831  dihglblem2aN  34957  dihintcl  35008  dvh1dim  35106
  Copyright terms: Public domain W3C validator