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

Theorem exlimddv 1649
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 425 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
43exlimdv 1647 . 2  |-  ( ph  ->  ( E. x ps 
->  ch ) )
51, 4mpd 15 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360   E.wex 1551
This theorem is referenced by:  fvmptdv2  5820  tfrlem9a  6649  erref  6927  domdifsn  7193  xpdom2  7205  domunsn  7259  mapdom1  7274  sucdom2  7305  fineqvlem  7325  fissuni  7413  fipreima  7414  indexfi  7416  brwdom2  7543  wdomtr  7545  unwdomg  7554  unxpwdom  7559  infdifsn  7613  isinffi  7881  ac5num  7919  numacn  7932  acndom  7934  acndom2  7937  fodomacn  7939  infpss  8099  ssfin4  8192  domfin4  8193  enfin2i  8203  fin23lem31  8225  fin23lem41  8234  axcclem  8339  canthp1lem1  8529  canthp1  8531  winafp  8574  wun0  8595  prlem936  8926  supmul  9978  supxrre  10908  infmxrre  10916  ixxub  10939  ixxlb  10940  isumltss  12630  eulerth  13174  ramub2  13384  mrieqv2d  13866  mreexexlem4d  13874  acsinfd  14608  acsdomd  14609  issubg2  14961  sylow1lem4  15237  sylow3  15269  prmcyg  15505  ablfaclem3  15647  lbspss  16156  lsmcv  16215  cygzn  16853  lmff  17367  tgcmp  17466  hauscmplem  17471  clscon  17495  2ndcsep  17524  1stcelcls  17526  ptcnplem  17655  txcn  17660  fbdmn0  17868  ptcmplem2  18086  ptcmplem3  18087  tsmsxplem1  18184  met2ndci  18554  nmoid  18778  phtpcer  19022  phtpcco2  19026  cmetcau  19244  iscmet3lem2  19247  bcthlem4  19282  bcthlem5  19283  ovolicc2lem2  19416  vitali  19507  mbfimaopnlem  19549  limciun  19783  vieta1lem2  20230  cusgrafi  21493  usgramaxsize  21498  isgrp2d  21825  minvecolem5  22385  esumcst  24457  erdsze2lem1  24891  erdsze2  24893  ptpcon  24922  cvmliftpht  25007  relexpindlem  25141  mblfinlem2  26246  mblfinlem3  26247  mblfinlem4  26248  filnetlem3  26411  sdclem1  26449  sstotbnd  26486  prdsbnd  26504  prdstotbnd  26505  heibor1lem  26520  bfp  26535  eldioph2lem1  26820  eldioph2lem2  26821  rencldnfilem  26883  kelac1  27140  enfixsn  27236  lbslcic  27290  hbt  27313  psgnunilem3  27398  cncmpmax  27681  stoweidlem28  27755  stoweidlem31  27758  stoweidlem46  27773  stoweidlem53  27780  stoweidlem59  27786  llnn0  30315  lplnn0N  30346  lvoln0N  30390  diaglbN  31855  diaintclN  31858  dibglbN  31966  dibintclN  31967  dihglblem2aN  32093  dihintcl  32144  dvh1dim  32242
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552
  Copyright terms: Public domain W3C validator