Theorem exlimdv 1700

Description: Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.) Remove dependencies on ax-6 1719, ax-7 1739. (Revised by Wolf Lammen, 4-Dec-2017.)

Hypothesis

Ref	Expression
exlimdv.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
exlimdv	|- ( ph -> ( E. x ps -> ch ) )

Distinct variable groups:   ch, x   ph, x

Allowed substitution hint:   ps( x)

Proof of Theorem exlimdv

Step	Hyp	Ref	Expression
1		exlimdv.1	. . 3 |- ( ph -> ( ps -> ch ) )
2	1	eximdv 1686	. 2 |- ( ph -> ( E. x ps -> E. x ch ) )
3		ax5e 1682	. 2 |- ( E. x ch -> ch )
4	2, 3	syl6 33	1 |- ( ph -> ( E. x ps -> ch ) )

Syntax hints:   -> wi 4   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-ex 1597

This theorem is referenced by:  exlimdvv  1701  exlimddv  1702  axc9lem1  1970  nfeqf  2018  ax12v2  2056  sbcom2  2173  ax12eq  2264  ax12el  2265  ax12inda  2271  ax12v2-o  2272  tpid3g  4142  sssn  4185  reusv2lem2  4649  ralxfr2d  4663  euotd  4748  wefrc  4873  wereu2  4876  onfr  4917  releldmb  5237  relelrnb  5238  elres  5309  iss  5321  dffv2  5940  dff3  6034  elunirn  6151  isomin  6221  isofrlem  6224  ovmpt4g  6409  soex  6727  f1oweALT  6768  op1steq  6826  fo2ndf  6890  mpt2xopynvov0g  6942  reldmtpos  6963  rntpos  6968  erdisj  7359  map0g  7458  resixpfo  7507  domdifsn  7600  xpdom3  7615  domunsncan  7617  enfixsn  7626  fodomr  7668  mapdom2  7688  mapdom3  7689  phplem4  7699  php3  7703  sucdom2  7714  pssnn  7738  ssfi  7740  domfi  7741  findcard2  7760  ac6sfi  7764  isfinite2  7778  xpfi  7791  domunfican  7793  fiint  7797  fodomfib  7800  mapfien2  7868  marypha1lem  7893  ordiso  7941  hartogslem1  7967  brwdom2  7999  wdomtr  8001  brwdom3  8008  unwdomg  8010  xpwdomg  8011  unxpwdom2  8014  inf3lem2  8046  epfrs  8162  tcmin  8172  cplem1  8307  pm54.43  8381  dfac8alem  8410  dfac8b  8412  dfac8clem  8413  ac10ct  8415  acni2  8427  acndom  8432  numwdom  8440  wdomfil  8442  wdomnumr  8445  iunfictbso  8495  dfac2  8511  dfac9  8516  kmlem13  8542  cdainf  8572  fictb  8625  cfeq0  8636  cff1  8638  cfflb  8639  cofsmo  8649  cfsmolem  8650  coftr  8653  infpssr  8688  fin4en1  8689  fin23lem7  8696  isf34lem4  8757  axcc3  8818  domtriomlem  8822  axdc2lem  8828  axdc3lem2  8831  axdc3lem4  8833  axdc4lem  8835  ac6num  8859  ttukeylem6  8894  ttukeyg  8897  fodomb  8904  iundom2g  8915  alephreg  8957  fpwwe2lem11  9018  fpwwe2lem12  9019  canthp1  9032  pwfseq  9042  gruen  9190  grudomon  9195  gruina  9196  grur1  9198  ltexnq  9353  ltbtwnnq  9356  genpn0  9381  psslinpr  9409  prlem934  9411  ltaddpr  9412  ltexprlem2  9415  ltexprlem6  9419  ltexprlem7  9420  reclem2pr  9426  reclem4pr  9428  suplem1pr  9430  sup2  10499  supmul1  10508  infmrcl  10522  negn0  11168  zsupss  11171  fiinfnf1o  12391  hashfun  12461  hashf1  12472  rlimdm  13337  climcau  13456  caucvgb  13465  summolem2  13501  zsum  13503  sumz  13507  fsumf1o  13508  fsumss  13510  fsumcl2lem  13516  fsumadd  13524  fsummulc2  13562  fsumconst  13568  fsumrelem  13584  ruclem13  13836  4sqlem12  14333  vdwapun  14351  vdwlem9  14366  vdwlem10  14367  ramz  14402  ramub1  14405  firest  14688  mremre  14859  isacs2  14908  iscatd2  14936  sscfn1  15047  sscfn2  15048  gsumval2a  15834  symggen  16301  cyggex2  16702  gsumval3OLD  16711  gsumval3  16714  gsumzres  16717  gsumzcl2  16718  gsumzf1o  16720  gsumzresOLD  16721  gsumzclOLD  16722  gsumzf1oOLD  16723  gsumzaddlem  16737  gsumzaddlemOLD  16739  gsumconst  16757  gsumzmhm  16760  gsumzmhmOLD  16761  gsumzoppg  16770  gsumzoppgOLD  16771  gsum2d2  16805  pgpfac1lem5  16932  ablfaclem3  16940  lss0cl  17393  lspsnat  17591  cnsubrg  18274  gsumfsum  18280  obslbs  18556  lmiclbs  18667  lmisfree  18672  mdetdiaglem  18895  mdet0  18903  eltg3  19258  tgtop  19269  tgidm  19276  ppttop  19302  toponmre  19388  tgrest  19454  neitr  19475  tgcn  19547  cmpsublem  19693  cmpsub  19694  iunconlem  19722  uncon  19724  1stcfb  19740  2ndcctbss  19750  2ndcdisj  19751  1stcelcls  19756  1stccnp  19757  1stckgen  19818  ptuni2  19840  ptbasfi  19845  ptpjopn  19876  ptclsg  19879  ptcnp  19886  prdstopn  19892  txindis  19898  txtube  19904  txcmplem1  19905  txcmplem2  19906  xkococnlem  19923  txcon  19953  trfbas2  20107  filtop  20119  filcon  20147  filssufilg  20175  fmfnfm  20222  ufldom  20226  hauspwpwf1  20251  alexsubALTlem3  20312  alexsubALT  20314  ptcmplem2  20316  tmdgsum2  20358  tgptsmscld  20416  ustfilxp  20478  xbln0  20680  opnreen  21099  metdsre  21120  cnheibor  21218  phtpc01  21259  cfilfcls  21476  cmetcaulem  21490  iscmet3  21495  ovolctb  21664  ovoliunlem3  21678  ovoliunnul  21681  ovolicc2lem5  21695  ovolicc2  21696  dyadmbl  21772  vitali  21785  itg11  21861  bddmulibl  22008  perfdvf  22070  dvcnp2  22086  dvlip  22157  dvne0  22175  fta1g  22331  fta1  22466  ulmcau  22552  pserulm  22579  wilthlem2  23099  dchrvmasumif  23444  rpvmasum2  23453  dchrisum0re  23454  dchrisum0lem3  23460  dchrisum0  23461  dchrmusum  23465  dchrvmasum  23466  axcontlem10  23980  usgrafisindb1  24113  wlkiswwlk  24402  wlklniswwlkn  24405  clwlkisclwwlklem0  24492  clwlkfoclwwlk  24549  frgra3vlem2  24705  spansncvi  26274  fmcncfil  27577  volmeas  27871  derangenlem  28283  cvmsss2  28387  cvmopnlem  28391  cvmfolem  28392  cvmliftmolem2  28395  cvmliftlem15  28411  cvmlift2lem10  28425  cvmlift3lem8  28439  rtrclreclem.trans  28572  ntrivcvg  28636  prodmolem2  28672  zprod  28674  prod1  28681  fprodf1o  28683  fprodss  28685  fprodcl2lem  28687  fprodmul  28695  fproddiv  28696  fprodconst  28713  fprodn0  28714  fundmpss  28801  frmin  28927  wfrlem12  28959  frrlem11  29004  nocvxmin  29056  wl-sbcom2d  29616  supaddc  29646  heicant  29654  itg2addnclem  29671  fnessref  29793  refssfne  29794  locfincmp  29804  comppfsc  29807  neibastop2lem  29809  neibastop2  29810  fnemeet2  29816  fnejoin2  29818  tailfb  29826  sdclem1  29867  fdc  29869  istotbnd3  29898  sstotbnd2  29901  prdsbnd2  29922  heibor1lem  29936  heiborlem1  29938  heiborlem10  29947  heibor  29948  riscer  30022  divrngidl  30056  prtlem17  30249  mapfien2OLD  30674  lptre2pt  31210  itgsubsticclem  31321  stoweidlem43  31371  stoweidlem48  31376  stoweidlem57  31385  stoweidlem60  31388  rlimdmafv  31757  usgo1s0ALT  31932  usgo1s0  31937  onfrALT  32419  chordthmALT  32831  bnj849  33080  bj-axc15v  33429  osumcllem8N  34777  pexmidlem5N  34788  mapdrvallem2  36460