Theorem exlimdv 1769

Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 1967. (Contributed by NM, 27-Apr-1994.) Remove dependencies on ax-6 1795, ax-7 1840. (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 1755	. 2 |- ( ph -> ( E. x ps -> E. x ch ) )
3		ax5e 1751	. 2 |- ( E. x ch -> ch )
4	2, 3	syl6 35	1 |- ( ph -> ( E. x ps -> ch ) )

Syntax hints:   -> wi 4   E.wex 1660

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749

This theorem depends on definitions:  df-bi 189  df-ex 1661

This theorem is referenced by:  exlimdvv  1770  exlimddv  1771  axc9lem1  2056  nfeqf  2101  ax12v2  2139  sbcom2  2241  tpid3g  4113  sssn  4156  reusv2lem2  4624  ralxfr2d  4635  euotd  4719  wefrc  4845  wereu2  4848  releldmb  5086  relelrnb  5087  elres  5157  iss  5169  onfr  5479  dffv2  5952  dff3  6048  elunirn  6169  fsnex  6194  f1prex  6195  isomin  6241  isofrlem  6244  ovmpt4g  6431  soex  6748  f1oweALT  6789  op1steq  6847  fo2ndf  6912  mpt2xopynvov0g  6966  reldmtpos  6987  rntpos  6992  wfrlem12  7053  wfrlem17  7058  erdisj  7417  map0g  7517  resixpfo  7566  domdifsn  7659  xpdom3  7674  domunsncan  7676  enfixsn  7685  fodomr  7727  mapdom2  7747  mapdom3  7748  phplem4  7758  php3  7762  sucdom2  7772  pssnn  7794  ssfi  7796  domfi  7797  findcard2  7815  ac6sfi  7819  isfinite2  7833  xpfi  7846  domunfican  7848  fiint  7852  fodomfib  7855  mapfien2  7926  marypha1lem  7951  ordiso  8035  hartogslem1  8061  brwdom2  8092  wdomtr  8094  brwdom3  8101  unwdomg  8103  xpwdomg  8104  unxpwdom2  8107  inf3lem2  8138  epfrs  8218  tcmin  8228  cplem1  8363  pm54.43  8437  dfac8alem  8462  dfac8b  8464  dfac8clem  8465  ac10ct  8467  acni2  8479  acndom  8484  numwdom  8492  wdomfil  8494  wdomnumr  8497  iunfictbso  8547  dfac2  8563  dfac9  8568  kmlem13  8594  cdainf  8624  fictb  8677  cfeq0  8688  cff1  8690  cfflb  8691  cofsmo  8701  cfsmolem  8702  coftr  8705  infpssr  8740  fin4en1  8741  fin23lem7  8748  isf34lem4  8809  axcc3  8870  domtriomlem  8874  axdc2lem  8880  axdc3lem2  8883  axdc3lem4  8885  axdc4lem  8887  ac6num  8911  ttukeylem6  8946  ttukeyg  8949  fodomb  8956  iundom2g  8967  alephreg  9009  fpwwe2lem11  9067  fpwwe2lem12  9068  canthp1  9081  pwfseq  9091  gruen  9239  grudomon  9244  gruina  9245  grur1  9247  ltexnq  9402  ltbtwnnq  9405  genpn0  9430  psslinpr  9458  prlem934  9460  ltaddpr  9461  ltexprlem2  9464  ltexprlem6  9468  ltexprlem7  9469  reclem2pr  9475  reclem4pr  9477  suplem1pr  9479  negn0  10050  sup2  10567  supaddc  10576  supmul1  10578  infmrclOLD  10595  zsupss  11255  fiinfnf1o  12534  hashfun  12608  hashf1  12619  rtrclreclem3  13117  rlimdm  13608  climcau  13727  caucvgb  13739  summolem2  13775  zsum  13777  sumz  13781  fsumf1o  13782  fsumss  13784  fsumcl2lem  13790  fsumadd  13798  fsummulc2  13838  fsumconst  13844  fsumrelem  13860  ntrivcvg  13946  prodmolem2  13982  zprod  13984  prod1  13991  fprodf1o  13993  fprodss  13995  fprodcl2lem  13997  fprodmul  14007  fproddiv  14008  fprodconst  14025  fprodn0  14026  ruclem13  14287  4sqlem12  14893  vdwapun  14917  vdwlem9  14932  vdwlem10  14933  ramz  14976  ramub1  14979  firest  15324  mremre  15503  isacs2  15552  iscatd2  15580  sscfn1  15715  sscfn2  15716  gsumval2a  16515  symggen  17104  cyggex2  17524  gsumval3  17534  gsumzres  17536  gsumzcl2  17537  gsumzf1o  17539  gsumzaddlem  17547  gsumconst  17560  gsumzmhm  17563  gsumzoppg  17570  gsum2d2  17599  pgpfac1lem5  17705  ablfaclem3  17713  lss0cl  18163  lspsnat  18361  cnsubrg  19021  gsumfsum  19027  obslbs  19285  lmiclbs  19387  lmisfree  19392  mdetdiaglem  19615  mdet0  19623  eltg3  19969  tgtop  19981  tgidm  19988  ppttop  20014  toponmre  20101  tgrest  20167  neitr  20188  tgcn  20260  cmpsublem  20406  cmpsub  20407  iunconlem  20434  uncon  20436  1stcfb  20452  2ndcctbss  20462  2ndcdisj  20463  1stcelcls  20468  1stccnp  20469  locfincmp  20533  comppfsc  20539  1stckgen  20561  ptuni2  20583  ptbasfi  20588  ptpjopn  20619  ptclsg  20622  ptcnp  20629  prdstopn  20635  txindis  20641  txtube  20647  txcmplem1  20648  txcmplem2  20649  xkococnlem  20666  txcon  20696  trfbas2  20850  filtop  20862  filcon  20890  filssufilg  20918  fmfnfm  20965  ufldom  20969  hauspwpwf1  20994  alexsubALTlem3  21056  alexsubALT  21058  ptcmplem2  21060  tmdgsum2  21103  tgptsmscld  21157  ustfilxp  21219  xbln0  21421  opnreen  21841  metdsre  21862  metdsreOLD  21877  cnheibor  21975  phtpc01  22019  cfilfcls  22236  cmetcaulem  22250  iscmet3  22255  ovolctb  22435  ovoliunlem3  22449  ovoliunnul  22452  ovolicc2lem5  22467  ovolicc2  22468  dyadmbl  22550  vitali  22563  itg11  22641  bddmulibl  22788  perfdvf  22850  dvcnp2  22866  dvlip  22937  dvne0  22955  fta1g  23110  fta1  23253  ulmcau  23342  pserulm  23369  wilthlem2  23986  dchrvmasumif  24333  rpvmasum2  24342  dchrisum0re  24343  dchrisum0lem3  24349  dchrisum0  24350  dchrmusum  24354  dchrvmasum  24355  axcontlem10  24995  usgrafisindb1  25129  wlkiswwlk  25418  wlklniswwlkn  25421  clwlkisclwwlklem0  25508  clwlkfoclwwlk  25565  frgra3vlem2  25721  spansncvi  27297  reff  28668  locfinreflem  28669  cmpcref  28679  fmcncfil  28739  volmeas  29056  omssubadd  29130  omssubaddOLD  29134  bnj849  29738  derangenlem  29896  cvmsss2  29999  cvmopnlem  30003  cvmfolem  30004  cvmliftmolem2  30007  cvmliftlem15  30023  cvmlift2lem10  30037  cvmlift3lem8  30051  fundmpss  30408  frmin  30481  frrlem11  30527  nocvxmin  30579  fnessref  31012  refssfne  31013  neibastop2lem  31015  neibastop2  31016  fnemeet2  31022  fnejoin2  31024  tailfb  31032  bj-axc15v  31323  wl-sbcom2d  31811  wl-ax12v3  31832  poimirlem25  31885  poimirlem27  31887  heicant  31895  itg2addnclem  31913  sdclem1  31992  fdc  31994  istotbnd3  32023  sstotbnd2  32026  prdsbnd2  32047  heibor1lem  32061  heiborlem1  32063  heiborlem10  32072  heibor  32073  riscer  32147  divrngidl  32181  prtlem17  32372  ax12eq  32437  ax12el  32438  ax12inda  32444  ax12v2-o  32445  osumcllem8N  33453  pexmidlem5N  33464  mapdrvallem2  35138  onfrALT  36779  chordthmALT  37197  ssnnf1octb  37326  inficc  37472  fsumnncl  37479  stoweidlem43  37730  stoweidlem48  37735  stoweidlem57  37744  stoweidlem60  37747  sge0cl  38017  nnfoctbdj  38079  ismeannd  38090  caragenunicl  38130  isomennd  38137  ovn0lem  38168  ovnsubaddlem2  38174  rlimdmafv  38397  usgr1v0e  38960  usgo1s0ALT  39053  usgo1s0  39058  mgmpropd  39079  c0snmgmhm  39218