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

Theorem exlimddv 1645
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 424 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
43exlimdv 1643 . 2  |-  ( ph  ->  ( E. x ps 
->  ch ) )
51, 4mpd 15 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359   E.wex 1547
This theorem is referenced by:  fvmptdv2  5777  tfrlem9a  6606  erref  6884  domdifsn  7150  xpdom2  7162  domunsn  7216  mapdom1  7231  sucdom2  7262  fineqvlem  7282  fissuni  7369  fipreima  7370  indexfi  7372  brwdom2  7497  wdomtr  7499  unwdomg  7508  unxpwdom  7513  infdifsn  7567  isinffi  7835  ac5num  7873  numacn  7886  acndom  7888  acndom2  7891  fodomacn  7893  infpss  8053  ssfin4  8146  domfin4  8147  enfin2i  8157  fin23lem31  8179  fin23lem41  8188  axcclem  8293  canthp1lem1  8483  canthp1  8485  winafp  8528  wun0  8549  prlem936  8880  supmul  9932  supxrre  10862  infmxrre  10870  ixxub  10893  ixxlb  10894  isumltss  12583  eulerth  13127  ramub2  13337  mrieqv2d  13819  mreexexlem4d  13827  acsinfd  14561  acsdomd  14562  issubg2  14914  sylow1lem4  15190  sylow3  15222  prmcyg  15458  ablfaclem3  15600  lbspss  16109  lsmcv  16168  cygzn  16806  lmff  17319  tgcmp  17418  hauscmplem  17423  clscon  17446  2ndcsep  17475  1stcelcls  17477  ptcnplem  17606  txcn  17611  fbdmn0  17819  ptcmplem2  18037  ptcmplem3  18038  tsmsxplem1  18135  met2ndci  18505  nmoid  18729  phtpcer  18973  phtpcco2  18977  cmetcau  19195  iscmet3lem2  19198  bcthlem4  19233  bcthlem5  19234  ovolicc2lem2  19367  vitali  19458  mbfimaopnlem  19500  limciun  19734  vieta1lem2  20181  cusgrafi  21444  usgramaxsize  21449  isgrp2d  21776  minvecolem5  22336  esumcst  24408  erdsze2lem1  24842  erdsze2  24844  ptpcon  24873  cvmliftpht  24958  relexpindlem  25092  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  filnetlem3  26299  sdclem1  26337  sstotbnd  26374  prdsbnd  26392  prdstotbnd  26393  heibor1lem  26408  bfp  26423  eldioph2lem1  26708  eldioph2lem2  26709  rencldnfilem  26771  kelac1  27029  enfixsn  27125  lbslcic  27179  hbt  27202  psgnunilem3  27287  cncmpmax  27570  stoweidlem28  27644  stoweidlem31  27647  stoweidlem46  27662  stoweidlem53  27669  stoweidlem59  27675  llnn0  29998  lplnn0N  30029  lvoln0N  30073  diaglbN  31538  diaintclN  31541  dibglbN  31649  dibintclN  31650  dihglblem2aN  31776  dihintcl  31827  dvh1dim  31925
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548
  Copyright terms: Public domain W3C validator