Theorem exlimdv 1690

Description: Deduction from Theorem 19.23 of [Margaris] p. 90. Revised to remove dependency on ax-6 1708 and ax-7 1728. (Contributed by NM, 27-Apr-1994.) (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 1676	. 2 |- ( ph -> ( E. x ps -> E. x ch ) )
3		ax5e 1672	. 2 |- ( E. x ch -> ch )
4	2, 3	syl6 33	1 |- ( ph -> ( E. x ps -> ch ) )

Syntax hints:   -> wi 4   E.wex 1586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670

This theorem depends on definitions:  df-bi 185  df-ex 1587

This theorem is referenced by:  exlimdvv  1691  exlimddv  1692  axc9lem1  1945  nfeqf  1993  ax12v2  2033  sbcom2  2151  ax12eq  2242  ax12el  2243  ax12inda  2249  ax12v2-o  2250  tpid3g  4011  sssn  4052  reusv2lem2  4515  ralxfr2d  4529  euotd  4613  wefrc  4735  wereu2  4738  onfr  4779  releldmb  5095  relelrnb  5096  elres  5166  iss  5175  dffv2  5785  dff3  5877  elunirn  5989  isomin  6049  isofrlem  6052  ovmpt4g  6234  soex  6542  f1oweALT  6582  op1steq  6639  fo2ndf  6700  mpt2xopynvov0g  6752  reldmtpos  6774  rntpos  6779  erdisj  7169  map0g  7273  resixpfo  7322  domdifsn  7415  xpdom3  7430  domunsncan  7432  enfixsn  7441  fodomr  7483  mapdom2  7503  mapdom3  7504  phplem4  7514  php3  7518  sucdom2  7528  pssnn  7552  ssfi  7554  domfi  7555  findcard2  7573  ac6sfi  7577  isfinite2  7591  xpfi  7604  domunfican  7605  fiint  7609  fodomfib  7612  mapfien2  7679  marypha1lem  7704  ordiso  7751  hartogslem1  7777  brwdom2  7809  wdomtr  7811  brwdom3  7818  unwdomg  7820  xpwdomg  7821  unxpwdom2  7824  inf3lem2  7856  epfrs  7972  tcmin  7982  cplem1  8117  pm54.43  8191  dfac8alem  8220  dfac8b  8222  dfac8clem  8223  ac10ct  8225  acni2  8237  acndom  8242  numwdom  8250  wdomfil  8252  wdomnumr  8255  iunfictbso  8305  dfac2  8321  dfac9  8326  kmlem13  8352  cdainf  8382  fictb  8435  cfeq0  8446  cff1  8448  cfflb  8449  cofsmo  8459  cfsmolem  8460  coftr  8463  infpssr  8498  fin4en1  8499  fin23lem7  8506  isf34lem4  8567  axcc3  8628  domtriomlem  8632  axdc2lem  8638  axdc3lem2  8641  axdc3lem4  8643  axdc4lem  8645  ac6num  8669  ttukeylem6  8704  ttukeyg  8707  fodomb  8714  iundom2g  8725  alephreg  8767  fpwwe2lem11  8828  fpwwe2lem12  8829  canthp1  8842  pwfseq  8852  gruen  9000  grudomon  9005  gruina  9006  grur1  9008  ltexnq  9165  ltbtwnnq  9168  genpn0  9193  psslinpr  9221  prlem934  9223  ltaddpr  9224  ltexprlem2  9227  ltexprlem6  9231  ltexprlem7  9232  reclem2pr  9238  reclem4pr  9240  suplem1pr  9242  sup2  10307  supmul1  10316  infmrcl  10330  negn0  10962  zsupss  10965  fiinfnf1o  12142  hashfun  12220  hashf1  12231  rlimdm  13050  climcau  13169  caucvgb  13178  summolem2  13214  zsum  13216  sumz  13220  fsumf1o  13221  fsumss  13223  fsumcl2lem  13229  fsumadd  13236  fsummulc2  13272  fsumconst  13278  fsumrelem  13291  ruclem13  13545  4sqlem12  14038  vdwapun  14056  vdwlem9  14071  vdwlem10  14072  ramz  14107  ramub1  14110  firest  14392  mremre  14563  isacs2  14612  iscatd2  14640  sscfn1  14751  sscfn2  14752  gsumval2a  15533  symggen  15997  cyggex2  16394  gsumval3OLD  16403  gsumval3  16406  gsumzres  16409  gsumzcl2  16410  gsumzf1o  16412  gsumzresOLD  16413  gsumzclOLD  16414  gsumzf1oOLD  16415  gsumzaddlem  16429  gsumzaddlemOLD  16431  gsumconst  16449  gsumzmhm  16452  gsumzmhmOLD  16453  gsumzoppg  16462  gsumzoppgOLD  16463  gsum2d2  16488  pgpfac1lem5  16602  ablfaclem3  16610  lss0cl  17050  lspsnat  17248  cnsubrg  17895  gsumfsum  17901  obslbs  18177  lmiclbs  18288  lmisfree  18293  mdet1  18430  eltg3  18589  tgtop  18600  tgidm  18607  ppttop  18633  toponmre  18719  tgrest  18785  neitr  18806  tgcn  18878  cmpsublem  19024  cmpsub  19025  iunconlem  19053  uncon  19055  1stcfb  19071  2ndcctbss  19081  2ndcdisj  19082  1stcelcls  19087  1stccnp  19088  1stckgen  19149  ptuni2  19171  ptbasfi  19176  ptpjopn  19207  ptclsg  19210  ptcnp  19217  prdstopn  19223  txindis  19229  txtube  19235  txcmplem1  19236  txcmplem2  19237  xkococnlem  19254  txcon  19284  trfbas2  19438  filtop  19450  filcon  19478  filssufilg  19506  fmfnfm  19553  ufldom  19557  hauspwpwf1  19582  alexsubALTlem3  19643  alexsubALT  19645  ptcmplem2  19647  tmdgsum2  19689  tgptsmscld  19747  ustfilxp  19809  xbln0  20011  opnreen  20430  metdsre  20451  cnheibor  20549  phtpc01  20590  cfilfcls  20807  cmetcaulem  20821  iscmet3  20826  ovolctb  20995  ovoliunlem3  21009  ovoliunnul  21012  ovolicc2lem5  21026  ovolicc2  21027  dyadmbl  21102  vitali  21115  itg11  21191  bddmulibl  21338  perfdvf  21400  dvcnp2  21416  dvlip  21487  dvne0  21505  fta1g  21661  fta1  21796  ulmcau  21882  pserulm  21909  wilthlem2  22429  dchrvmasumif  22774  rpvmasum2  22783  dchrisum0re  22784  dchrisum0lem3  22790  dchrisum0  22791  dchrmusum  22795  dchrvmasum  22796  axcontlem10  23241  usgrafisindb1  23344  spansncvi  25077  fmcncfil  26383  volmeas  26669  derangenlem  27081  cvmsss2  27185  cvmopnlem  27189  cvmfolem  27190  cvmliftmolem2  27193  cvmliftlem15  27209  cvmlift2lem10  27223  cvmlift3lem8  27237  rtrclreclem.trans  27370  ntrivcvg  27434  prodmolem2  27470  zprod  27472  prod1  27479  fprodf1o  27481  fprodss  27483  fprodcl2lem  27485  fprodmul  27493  fproddiv  27494  fprodconst  27511  fprodn0  27512  fundmpss  27599  frmin  27725  wfrlem12  27757  frrlem11  27802  nocvxmin  27854  wl-sbcom2d  28413  supaddc  28443  heicant  28452  itg2addnclem  28469  fnessref  28591  refssfne  28592  locfincmp  28602  comppfsc  28605  neibastop2lem  28607  neibastop2  28608  fnemeet2  28614  fnejoin2  28616  tailfb  28624  sdclem1  28665  fdc  28667  istotbnd3  28696  sstotbnd2  28699  prdsbnd2  28720  heibor1lem  28734  heiborlem1  28736  heiborlem10  28745  heibor  28746  riscer  28820  divrngidl  28854  prtlem17  29047  mapfien2OLD  29475  stoweidlem43  29864  stoweidlem48  29869  stoweidlem57  29878  stoweidlem60  29881  rlimdmafv  30109  wlkiswwlk  30358  wlklniswwlkn  30361  clwlkisclwwlklem0  30476  clwlkfoclwwlk  30544  frgra3vlem2  30619  mdet0  30930  mdetdiaglem  30932  onfrALT  31353  chordthmALT  31765  bnj849  32014  bj-axc15v  32361  osumcllem8N  33703  pexmidlem5N  33714  mapdrvallem2  35386