Theorem exlimdv 1643

Description: Deduction from Theorem 19.23 of [Margaris] p. 90. Revised to remove dependency on ax-9 1662 and ax-8 1683. (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 1629	. 2 |- ( ph -> ( E. x ps -> E. x ch ) )
3		ax17e 1625	. 2 |- ( E. x ch -> ch )
4	2, 3	syl6 31	1 |- ( ph -> ( E. x ps -> ch ) )

Syntax hints:   -> wi 4   E.wex 1547

This theorem is referenced by:  exlimdvv  1644  exlimddv  1645  ax10OLD  1998  ax11v2  2045  ax11eq  2243  ax11el  2244  ax11inda  2250  ax11v2-o  2251  tpid3g  3879  sssn  3917  euotd  4417  wefrc  4536  wereu2  4539  onfr  4580  reusv2lem2  4684  ralxfr2d  4698  releldmb  5063  relelrnb  5064  elres  5140  iss  5148  soex  5278  dffv2  5755  dff3  5841  elunirnALT  5959  isomin  6016  isofrlem  6019  f1oweALT  6033  ovmpt4g  6155  op1steq  6350  fo2ndf  6412  mpt2xopynvov0g  6424  reldmtpos  6446  rntpos  6451  erdisj  6911  map0g  7012  resixpfo  7059  domdifsn  7150  xpdom3  7165  domunsncan  7167  fodomr  7217  mapdom2  7237  mapdom3  7238  phplem4  7248  php3  7252  sucdom2  7262  pssnn  7286  ssfi  7288  domfi  7289  findcard2  7307  ac6sfi  7310  isfinite2  7324  xpfi  7337  domunfican  7338  fiint  7342  fodomfib  7345  marypha1lem  7396  ordiso  7441  hartogslem1  7467  brwdom2  7497  wdomtr  7499  brwdom3  7506  unwdomg  7508  xpwdomg  7509  unxpwdom2  7512  inf3lem2  7540  epfrs  7623  tcmin  7636  cplem1  7769  pm54.43  7843  dfac8alem  7866  dfac8b  7868  dfac8clem  7869  ac10ct  7871  acni2  7883  acndom  7888  numwdom  7896  wdomfil  7898  wdomnumr  7901  iunfictbso  7951  dfac2  7967  dfac9  7972  kmlem13  7998  cdainf  8028  fictb  8081  cfeq0  8092  cff1  8094  cfflb  8095  cofsmo  8105  cfsmolem  8106  coftr  8109  infpssr  8144  fin4en1  8145  fin23lem7  8152  isf34lem4  8213  axcc3  8274  domtriomlem  8278  axdc2lem  8284  axdc3lem2  8287  axdc3lem4  8289  axdc4lem  8291  ac6num  8315  ttukeylem6  8350  ttukeyg  8353  fodomb  8360  iundom2g  8371  alephreg  8413  fpwwe2lem11  8471  fpwwe2lem12  8472  canthp1  8485  pwfseq  8495  gruen  8643  grudomon  8648  gruina  8649  grur1  8651  ltexnq  8808  ltbtwnnq  8811  genpn0  8836  psslinpr  8864  prlem934  8866  ltaddpr  8867  ltexprlem2  8870  ltexprlem6  8874  ltexprlem7  8875  reclem2pr  8881  reclem4pr  8883  suplem1pr  8885  sup2  9920  supmul1  9929  infmrcl  9943  negn0  10518  zsupss  10521  fiinfnf1o  11589  hashfun  11655  hashf1  11661  rlimdm  12300  climcau  12419  caucvgb  12428  summolem2  12465  zsum  12467  sumz  12471  fsumf1o  12472  fsumss  12474  fsumcl2lem  12480  fsumadd  12487  fsummulc2  12522  fsumconst  12528  fsumrelem  12541  ruclem13  12796  4sqlem12  13279  vdwapun  13297  vdwlem9  13312  vdwlem10  13313  ramz  13348  ramub1  13351  firest  13615  mremre  13784  isacs2  13833  iscatd2  13861  sscfn1  13972  sscfn2  13973  gsumval2a  14737  cyggex2  15461  gsumval3  15469  gsumzres  15472  gsumzcl  15473  gsumzf1o  15474  gsumzaddlem  15481  gsumconst  15487  gsumzmhm  15488  gsumzoppg  15494  gsum2d2  15503  pgpfac1lem5  15592  ablfaclem3  15600  lss0cl  15978  lspsnat  16172  cnsubrg  16714  gsumfsum  16721  obslbs  16912  eltg3  16982  tgtop  16993  tgidm  17000  ppttop  17026  toponmre  17112  tgrest  17177  neitr  17198  tgcn  17270  cmpsublem  17416  cmpsub  17417  iunconlem  17443  uncon  17445  1stcfb  17461  2ndcctbss  17471  2ndcdisj  17472  1stcelcls  17477  1stccnp  17478  1stckgen  17539  ptuni2  17561  ptbasfi  17566  ptpjopn  17597  ptclsg  17600  ptcnp  17607  prdstopn  17613  txindis  17619  txtube  17625  txcmplem1  17626  txcmplem2  17627  xkococnlem  17644  txcon  17674  trfbas2  17828  filtop  17840  filcon  17868  filssufilg  17896  fmfnfm  17943  ufldom  17947  hauspwpwf1  17972  alexsubALTlem3  18033  alexsubALT  18035  ptcmplem2  18037  tmdgsum2  18079  tgptsmscld  18133  ustfilxp  18195  xbln0  18397  opnreen  18815  metdsre  18836  cnheibor  18933  phtpc01  18974  cfilfcls  19180  cmetcaulem  19194  iscmet3  19199  ovolctb  19339  ovoliunlem3  19353  ovoliunnul  19356  ovolicc2lem5  19370  ovolicc2  19371  dyadmbl  19445  vitali  19458  itg11  19536  bddmulibl  19683  perfdvf  19743  dvcnp2  19759  dvlip  19830  dvne0  19848  fta1g  20043  fta1  20178  ulmcau  20264  pserulm  20291  wilthlem2  20805  dchrvmasumif  21150  rpvmasum2  21159  dchrisum0re  21160  dchrisum0lem3  21166  dchrisum0  21167  dchrmusum  21171  dchrvmasum  21172  usgrafisindb1  21376  spansncvi  23107  fmcncfil  24270  volmeas  24540  derangenlem  24810  cvmsss2  24914  cvmopnlem  24918  cvmfolem  24919  cvmliftmolem2  24922  cvmliftlem15  24938  cvmlift2lem10  24952  cvmlift3lem8  24966  rtrclreclem.trans  25099  ntrivcvg  25178  prodmolem2  25214  zprod  25216  prod1  25223  fprodf1o  25225  fprodss  25227  fprodcl2lem  25229  fprodmul  25237  fproddiv  25238  fprodconst  25255  fprodn0  25256  fundmpss  25336  frmin  25456  wfrlem12  25481  frrlem11  25507  nocvxmin  25559  axcontlem10  25816  supaddc  26137  itg2addnclem  26155  fnessref  26263  refssfne  26264  locfincmp  26274  comppfsc  26277  neibastop2lem  26279  neibastop2  26280  fnemeet2  26286  fnejoin2  26288  tailfb  26296  sdclem1  26337  fdc  26339  istotbnd3  26370  sstotbnd2  26373  prdsbnd2  26394  heibor1lem  26408  heiborlem1  26410  heiborlem10  26419  heibor  26420  riscer  26494  divrngidl  26528  prtlem17  26615  enfixsn  27125  mapfien2  27126  lmiclbs  27175  lmisfree  27180  symggen  27279  stoweidlem43  27659  stoweidlem48  27664  stoweidlem57  27673  stoweidlem60  27676  rlimdmafv  27908  frgra3vlem2  28105  onfrALT  28346  chordthmALT  28755  bnj849  29002  ax10NEW7  29179  ax11v2NEW7  29234  osumcllem8N  30445  pexmidlem5N  30456  mapdrvallem2  32128

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-ex 1548