Theorem exlimddv 1726

Description: Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)

Hypotheses

Ref	Expression
exlimddv.1
exlimddv.2

Assertion

Ref	Expression
exlimddv

Distinct variable groups:   ,   ,

Proof of Theorem exlimddv

Step	Hyp	Ref	Expression
1		exlimddv.1	. 2
2		exlimddv.2	. . . 4
3	2	ex 434	. . 3
4	3	exlimdv 1724	. 2
5	1, 4	mpd 15	1

Syntax hints:  ->wi 4  /\wa 369  E.wex 1612

This theorem is referenced by:  fvmptdv2  5969  tfrlem9a  7074  erref  7350  domdifsn  7620  xpdom2  7632  enfixsn  7646  domunsn  7687  mapdom1  7702  sucdom2  7734  fineqvlem  7754  fissuni  7845  fipreima  7846  indexfi  7848  brwdom2  8020  wdomtr  8022  unwdomg  8031  unxpwdom  8036  infdifsn  8094  isinffi  8394  ac5num  8438  numacn  8451  acndom  8453  acndom2  8456  fodomacn  8458  infpss  8618  ssfin4  8711  domfin4  8712  enfin2i  8722  fin23lem31  8744  fin23lem41  8753  axcclem  8858  canthp1lem1  9051  canthp1  9053  winafp  9096  wun0  9117  prlem936  9446  supmul  10536  supxrre  11548  infmxrre  11556  ixxub  11579  ixxlb  11580  isumltss  13660  eulerth  14313  ramub2  14532  mrieqv2d  15036  mreexexlem4d  15044  acsinfd  15810  acsdomd  15811  issubg2  16216  psgnunilem3  16521  sylow1lem4  16621  sylow3  16653  prmcyg  16896  ablfaclem3  17138  lbspss  17728  lsmcv  17787  cygzn  18609  lbslcic  18876  lmff  19802  tgcmp  19901  hauscmplem  19906  clscon  19931  2ndcsep  19960  1stcelcls  19962  ptcnplem  20122  txcn  20127  fbdmn0  20335  ptcmplem2  20553  ptcmplem3  20554  tsmsxplem1  20655  met2ndci  21025  nmoid  21249  phtpcer  21495  phtpcco2  21499  cmetcau  21728  iscmet3lem2  21731  bcthlem4  21766  bcthlem5  21767  ovolicc2lem2  21929  vitali  22022  mbfimaopnlem  22062  limciun  22298  vieta1lem2  22707  tgldim0eq  23894  hpgerlem  24134  cusgrafi  24482  usgramaxsize  24487  isgrp2d  25237  minvecolem5  25797  foresf1o  27403  locfinref  27844  esumcst  28071  erdsze2lem1  28647  erdsze2  28649  ptpcon  28678  cvmliftpht  28763  relexpindlem  29062  mblfinlem2  30052  mblfinlem3  30053  mblfinlem4  30054  filnetlem3  30198  sdclem1  30236  sstotbnd  30271  prdsbnd  30289  prdstotbnd  30290  heibor1lem  30305  bfp  30320  eldioph2lem1  30693  eldioph2lem2  30694  rencldnfilem  30754  kelac1  31009  hbt  31079  cncmpmax  31407  lptre2pt  31646  itgsubsticclem  31774  stoweidlem28  31810  stoweidlem31  31813  stoweidlem46  31828  stoweidlem53  31835  stoweidlem59  31841  llnn0  35240  lplnn0N  35271  lvoln0N  35315  diaglbN  36782  diaintclN  36785  dibglbN  36893  dibintclN  36894  dihglblem2aN  37020  dihintcl  37071  dvh1dim  37169

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613