Theorem exlimdv 1689

Description: Deduction from Theorem 19.23 of [Margaris] p. 90. Revised to remove dependency on ax-6 1707 and ax-7 1727. (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 1675	. 2 |- ( ph -> ( E. x ps -> E. x ch ) )
3		ax5e 1671	. 2 |- ( E. x ch -> ch )
4	2, 3	syl6 33	1 |- ( ph -> ( E. x ps -> ch ) )

Syntax hints:   -> wi 4   E.wex 1589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669

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

This theorem is referenced by:  exlimdvv  1690  exlimddv  1691  axc9lem1  1944  nfeqf  1992  ax12v2  2032  sbcom2  2153  ax12eq  2243  ax12el  2244  ax12inda  2250  ax12v2-o  2251  tpid3g  3978  sssn  4019  reusv2lem2  4482  ralxfr2d  4496  euotd  4580  wefrc  4701  wereu2  4704  onfr  4745  releldmb  5061  relelrnb  5062  elres  5133  iss  5142  dffv2  5752  dff3  5844  elunirnALT  5957  isomin  6015  isofrlem  6018  ovmpt4g  6202  soex  6510  f1oweALT  6550  op1steq  6607  fo2ndf  6668  mpt2xopynvov0g  6720  reldmtpos  6742  rntpos  6747  erdisj  7136  map0g  7240  resixpfo  7289  domdifsn  7382  xpdom3  7397  domunsncan  7399  enfixsn  7408  fodomr  7450  mapdom2  7470  mapdom3  7471  phplem4  7481  php3  7485  sucdom2  7495  pssnn  7519  ssfi  7521  domfi  7522  findcard2  7540  ac6sfi  7544  isfinite2  7558  xpfi  7571  domunfican  7572  fiint  7576  fodomfib  7579  mapfien2  7646  marypha1lem  7671  ordiso  7718  hartogslem1  7744  brwdom2  7776  wdomtr  7778  brwdom3  7785  unwdomg  7787  xpwdomg  7788  unxpwdom2  7791  inf3lem2  7823  epfrs  7939  tcmin  7949  cplem1  8084  pm54.43  8158  dfac8alem  8187  dfac8b  8189  dfac8clem  8190  ac10ct  8192  acni2  8204  acndom  8209  numwdom  8217  wdomfil  8219  wdomnumr  8222  iunfictbso  8272  dfac2  8288  dfac9  8293  kmlem13  8319  cdainf  8349  fictb  8402  cfeq0  8413  cff1  8415  cfflb  8416  cofsmo  8426  cfsmolem  8427  coftr  8430  infpssr  8465  fin4en1  8466  fin23lem7  8473  isf34lem4  8534  axcc3  8595  domtriomlem  8599  axdc2lem  8605  axdc3lem2  8608  axdc3lem4  8610  axdc4lem  8612  ac6num  8636  ttukeylem6  8671  ttukeyg  8674  fodomb  8681  iundom2g  8692  alephreg  8734  fpwwe2lem11  8794  fpwwe2lem12  8795  canthp1  8808  pwfseq  8818  gruen  8966  grudomon  8971  gruina  8972  grur1  8974  ltexnq  9131  ltbtwnnq  9134  genpn0  9159  psslinpr  9187  prlem934  9189  ltaddpr  9190  ltexprlem2  9193  ltexprlem6  9197  ltexprlem7  9198  reclem2pr  9204  reclem4pr  9206  suplem1pr  9208  sup2  10273  supmul1  10282  infmrcl  10296  negn0  10928  zsupss  10931  fiinfnf1o  12104  hashfun  12182  hashf1  12193  rlimdm  13012  climcau  13131  caucvgb  13140  summolem2  13176  zsum  13178  sumz  13182  fsumf1o  13183  fsumss  13185  fsumcl2lem  13191  fsumadd  13198  fsummulc2  13233  fsumconst  13239  fsumrelem  13252  ruclem13  13506  4sqlem12  13999  vdwapun  14017  vdwlem9  14032  vdwlem10  14033  ramz  14068  ramub1  14071  firest  14353  mremre  14524  isacs2  14573  iscatd2  14601  sscfn1  14712  sscfn2  14713  gsumval2a  15491  symggen  15955  cyggex2  16352  gsumval3OLD  16361  gsumval3  16364  gsumzres  16367  gsumzcl2  16368  gsumzf1o  16370  gsumzresOLD  16371  gsumzclOLD  16372  gsumzf1oOLD  16373  gsumzaddlem  16387  gsumzaddlemOLD  16389  gsumconst  16405  gsumzmhm  16406  gsumzmhmOLD  16407  gsumzoppg  16415  gsumzoppgOLD  16416  gsum2d2  16439  pgpfac1lem5  16553  ablfaclem3  16561  lss0cl  16949  lspsnat  17147  cnsubrg  17716  gsumfsum  17722  obslbs  17996  lmiclbs  18107  lmisfree  18112  mdet1  18249  eltg3  18408  tgtop  18419  tgidm  18426  ppttop  18452  toponmre  18538  tgrest  18604  neitr  18625  tgcn  18697  cmpsublem  18843  cmpsub  18844  iunconlem  18872  uncon  18874  1stcfb  18890  2ndcctbss  18900  2ndcdisj  18901  1stcelcls  18906  1stccnp  18907  1stckgen  18968  ptuni2  18990  ptbasfi  18995  ptpjopn  19026  ptclsg  19029  ptcnp  19036  prdstopn  19042  txindis  19048  txtube  19054  txcmplem1  19055  txcmplem2  19056  xkococnlem  19073  txcon  19103  trfbas2  19257  filtop  19269  filcon  19297  filssufilg  19325  fmfnfm  19372  ufldom  19376  hauspwpwf1  19401  alexsubALTlem3  19462  alexsubALT  19464  ptcmplem2  19466  tmdgsum2  19508  tgptsmscld  19566  ustfilxp  19628  xbln0  19830  opnreen  20249  metdsre  20270  cnheibor  20368  phtpc01  20409  cfilfcls  20626  cmetcaulem  20640  iscmet3  20645  ovolctb  20814  ovoliunlem3  20828  ovoliunnul  20831  ovolicc2lem5  20845  ovolicc2  20846  dyadmbl  20921  vitali  20934  itg11  21010  bddmulibl  21157  perfdvf  21219  dvcnp2  21235  dvlip  21306  dvne0  21324  fta1g  21523  fta1  21658  ulmcau  21744  pserulm  21771  wilthlem2  22291  dchrvmasumif  22636  rpvmasum2  22645  dchrisum0re  22646  dchrisum0lem3  22652  dchrisum0  22653  dchrmusum  22657  dchrvmasum  22658  axcontlem10  23041  usgrafisindb1  23144  spansncvi  24877  fmcncfil  26214  volmeas  26500  derangenlem  26906  cvmsss2  27010  cvmopnlem  27014  cvmfolem  27015  cvmliftmolem2  27018  cvmliftlem15  27034  cvmlift2lem10  27048  cvmlift3lem8  27062  rtrclreclem.trans  27194  ntrivcvg  27258  prodmolem2  27294  zprod  27296  prod1  27303  fprodf1o  27305  fprodss  27307  fprodcl2lem  27309  fprodmul  27317  fproddiv  27318  fprodconst  27335  fprodn0  27336  fundmpss  27423  frmin  27549  wfrlem12  27581  frrlem11  27626  nocvxmin  27678  wl-sbcom2d  28233  supaddc  28258  heicant  28267  itg2addnclem  28284  fnessref  28406  refssfne  28407  locfincmp  28417  comppfsc  28420  neibastop2lem  28422  neibastop2  28423  fnemeet2  28429  fnejoin2  28431  tailfb  28439  sdclem1  28480  fdc  28482  istotbnd3  28511  sstotbnd2  28514  prdsbnd2  28535  heibor1lem  28549  heiborlem1  28551  heiborlem10  28560  heibor  28561  riscer  28635  divrngidl  28669  prtlem17  28863  mapfien2OLD  29291  stoweidlem43  29681  stoweidlem48  29686  stoweidlem57  29695  stoweidlem60  29698  rlimdmafv  29926  wlkiswwlk  30175  wlklniswwlkn  30178  clwlkisclwwlklem0  30293  clwlkfoclwwlk  30361  frgra3vlem2  30436  onfrALT  30955  chordthmALT  31368  bnj849  31617  bj-axc15v  31893  osumcllem8N  33177  pexmidlem5N  33188  mapdrvallem2  34860