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

Theorem exlimddv 1702
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 1700 . 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 1596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597
This theorem is referenced by:  fvmptdv2  5961  tfrlem9a  7052  erref  7328  domdifsn  7597  xpdom2  7609  enfixsn  7623  domunsn  7664  mapdom1  7679  sucdom2  7711  fineqvlem  7731  fissuni  7821  fipreima  7822  indexfi  7824  brwdom2  7995  wdomtr  7997  unwdomg  8006  unxpwdom  8011  infdifsn  8069  isinffi  8369  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  9026  canthp1  9028  winafp  9071  wun0  9092  prlem936  9421  supmul  10507  supxrre  11515  infmxrre  11523  ixxub  11546  ixxlb  11547  isumltss  13619  eulerth  14168  ramub2  14387  mrieqv2d  14890  mreexexlem4d  14898  acsinfd  15663  acsdomd  15664  issubg2  16011  psgnunilem3  16317  sylow1lem4  16417  sylow3  16449  prmcyg  16687  ablfaclem3  16928  lbspss  17511  lsmcv  17570  cygzn  18376  lbslcic  18643  lmff  19568  tgcmp  19667  hauscmplem  19672  clscon  19697  2ndcsep  19726  1stcelcls  19728  ptcnplem  19857  txcn  19862  fbdmn0  20070  ptcmplem2  20288  ptcmplem3  20289  tsmsxplem1  20390  met2ndci  20760  nmoid  20984  phtpcer  21230  phtpcco2  21234  cmetcau  21463  iscmet3lem2  21466  bcthlem4  21501  bcthlem5  21502  ovolicc2lem2  21664  vitali  21757  mbfimaopnlem  21797  limciun  22033  vieta1lem2  22441  cusgrafi  24158  usgramaxsize  24163  isgrp2d  24913  minvecolem5  25473  esumcst  27711  erdsze2lem1  28287  erdsze2  28289  ptpcon  28318  cvmliftpht  28403  relexpindlem  28537  mblfinlem2  29629  mblfinlem3  29630  mblfinlem4  29631  filnetlem3  29801  sdclem1  29839  sstotbnd  29874  prdsbnd  29892  prdstotbnd  29893  heibor1lem  29908  bfp  29923  eldioph2lem1  30297  eldioph2lem2  30298  rencldnfilem  30358  kelac1  30613  hbt  30683  cncmpmax  30985  stoweidlem28  31328  stoweidlem31  31331  stoweidlem46  31346  stoweidlem53  31353  stoweidlem59  31359  llnn0  34312  lplnn0N  34343  lvoln0N  34387  diaglbN  35852  diaintclN  35855  dibglbN  35963  dibintclN  35964  dihglblem2aN  36090  dihintcl  36141  dvh1dim  36239
  Copyright terms: Public domain W3C validator