Theorem exlimdv 1779

Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 1993. (Contributed by NM, 27-Apr-1994.) Remove dependencies on ax-6 1805, ax-7 1851. (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 1764	. 2 |- ( ph -> ( E. x ps -> E. x ch ) )
3		ax5e 1760	. 2 |- ( E. x ch -> ch )
4	2, 3	syl6 34	1 |- ( ph -> ( E. x ps -> ch ) )

Syntax hints:   -> wi 4   E.wex 1663

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

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

This theorem is referenced by:  exlimdvv  1780  exlimddv  1781  axc9lem1  2093  nfeqf  2139  ax12v2  2175  sbcom2  2274  tpid3g  4087  sssn  4130  elpreqprb  4162  reusv2lem2  4605  ralxfr2d  4616  euotd  4702  wefrc  4828  wereu2  4831  releldmb  5069  relelrnb  5070  elres  5140  iss  5152  onfr  5462  dffv2  5938  dff3  6035  elunirn  6156  fsnex  6181  f1prex  6182  isomin  6228  isofrlem  6231  ovmpt4g  6419  soex  6736  f1oweALT  6777  op1steq  6835  fo2ndf  6903  mpt2xopynvov0g  6960  reldmtpos  6981  rntpos  6986  wfrlem12  7047  wfrlem17  7052  erdisj  7411  map0g  7511  resixpfo  7560  domdifsn  7655  xpdom3  7670  domunsncan  7672  enfixsn  7681  fodomr  7723  mapdom2  7743  mapdom3  7744  phplem4  7754  php3  7758  sucdom2  7768  pssnn  7790  ssfi  7792  domfi  7793  findcard2  7811  ac6sfi  7815  isfinite2  7829  xpfi  7842  domunfican  7844  fiint  7848  fodomfib  7851  mapfien2  7922  marypha1lem  7947  ordiso  8031  hartogslem1  8057  brwdom2  8088  wdomtr  8090  brwdom3  8097  unwdomg  8099  xpwdomg  8100  unxpwdom2  8103  inf3lem2  8134  epfrs  8215  tcmin  8225  cplem1  8360  pm54.43  8434  dfac8alem  8460  dfac8b  8462  dfac8clem  8463  ac10ct  8465  acni2  8477  acndom  8482  numwdom  8490  wdomfil  8492  wdomnumr  8495  iunfictbso  8545  dfac2  8561  dfac9  8566  kmlem13  8592  cdainf  8622  fictb  8675  cfeq0  8686  cff1  8688  cfflb  8689  cofsmo  8699  cfsmolem  8700  coftr  8703  infpssr  8738  fin4en1  8739  fin23lem7  8746  isf34lem4  8807  axcc3  8868  domtriomlem  8872  axdc2lem  8878  axdc3lem2  8881  axdc3lem4  8883  axdc4lem  8885  ac6num  8909  ttukeylem6  8944  ttukeyg  8947  fodomb  8954  iundom2g  8965  alephreg  9007  fpwwe2lem11  9065  fpwwe2lem12  9066  canthp1  9079  pwfseq  9089  gruen  9237  grudomon  9242  gruina  9243  grur1  9245  ltexnq  9400  ltbtwnnq  9403  genpn0  9428  psslinpr  9456  prlem934  9458  ltaddpr  9459  ltexprlem2  9462  ltexprlem6  9466  ltexprlem7  9467  reclem2pr  9473  reclem4pr  9475  suplem1pr  9477  negn0  10048  sup2  10565  supaddc  10574  supmul1  10576  infmrclOLD  10593  zsupss  11253  fiinfnf1o  12533  hashfun  12609  hashf1  12620  rtrclreclem3  13123  rlimdm  13615  climcau  13734  caucvgb  13746  summolem2  13782  zsum  13784  sumz  13788  fsumf1o  13789  fsumss  13791  fsumcl2lem  13797  fsumadd  13805  fsummulc2  13845  fsumconst  13851  fsumrelem  13867  ntrivcvg  13953  prodmolem2  13989  zprod  13991  prod1  13998  fprodf1o  14000  fprodss  14002  fprodcl2lem  14004  fprodmul  14014  fproddiv  14015  fprodconst  14032  fprodn0  14033  ruclem13  14294  4sqlem12  14900  vdwapun  14924  vdwlem9  14939  vdwlem10  14940  ramz  14983  ramub1  14986  firest  15331  mremre  15510  isacs2  15559  iscatd2  15587  sscfn1  15722  sscfn2  15723  gsumval2a  16522  symggen  17111  cyggex2  17531  gsumval3  17541  gsumzres  17543  gsumzcl2  17544  gsumzf1o  17546  gsumzaddlem  17554  gsumconst  17567  gsumzmhm  17570  gsumzoppg  17577  gsum2d2  17606  pgpfac1lem5  17712  ablfaclem3  17720  lss0cl  18170  lspsnat  18368  cnsubrg  19028  gsumfsum  19034  obslbs  19293  lmiclbs  19395  lmisfree  19400  mdetdiaglem  19623  mdet0  19631  eltg3  19977  tgtop  19989  tgidm  19996  ppttop  20022  toponmre  20109  tgrest  20175  neitr  20196  tgcn  20268  cmpsublem  20414  cmpsub  20415  iunconlem  20442  uncon  20444  1stcfb  20460  2ndcctbss  20470  2ndcdisj  20471  1stcelcls  20476  1stccnp  20477  locfincmp  20541  comppfsc  20547  1stckgen  20569  ptuni2  20591  ptbasfi  20596  ptpjopn  20627  ptclsg  20630  ptcnp  20637  prdstopn  20643  txindis  20649  txtube  20655  txcmplem1  20656  txcmplem2  20657  xkococnlem  20674  txcon  20704  trfbas2  20858  filtop  20870  filcon  20898  filssufilg  20926  fmfnfm  20973  ufldom  20977  hauspwpwf1  21002  alexsubALTlem3  21064  alexsubALT  21066  ptcmplem2  21068  tmdgsum2  21111  tgptsmscld  21165  ustfilxp  21227  xbln0  21429  opnreen  21849  metdsre  21870  metdsreOLD  21885  cnheibor  21983  phtpc01  22027  cfilfcls  22244  cmetcaulem  22258  iscmet3  22263  ovolctb  22443  ovoliunlem3  22457  ovoliunnul  22460  ovolicc2lem5  22475  ovolicc2  22476  dyadmbl  22558  vitali  22571  itg11  22649  bddmulibl  22796  perfdvf  22858  dvcnp2  22874  dvlip  22945  dvne0  22963  fta1g  23118  fta1  23261  ulmcau  23350  pserulm  23377  wilthlem2  23994  dchrvmasumif  24341  rpvmasum2  24350  dchrisum0re  24351  dchrisum0lem3  24357  dchrisum0  24358  dchrmusum  24362  dchrvmasum  24363  axcontlem10  25003  usgrafisindb1  25137  wlkiswwlk  25426  wlklniswwlkn  25429  clwlkisclwwlklem0  25516  clwlkfoclwwlk  25573  frgra3vlem2  25729  spansncvi  27305  reff  28666  locfinreflem  28667  cmpcref  28677  fmcncfil  28737  volmeas  29054  omssubadd  29128  omssubaddOLD  29132  bnj849  29736  derangenlem  29894  cvmsss2  29997  cvmopnlem  30001  cvmfolem  30002  cvmliftmolem2  30005  cvmliftlem15  30021  cvmlift2lem10  30035  cvmlift3lem8  30049  fundmpss  30407  frmin  30480  frrlem11  30526  nocvxmin  30580  fnessref  31013  refssfne  31014  neibastop2lem  31016  neibastop2  31017  fnemeet2  31023  fnejoin2  31025  tailfb  31033  bj-axc15v  31362  wl-sbcom2d  31891  wl-ax12v3  31912  poimirlem25  31965  poimirlem27  31967  heicant  31975  itg2addnclem  31993  sdclem1  32072  fdc  32074  istotbnd3  32103  sstotbnd2  32106  prdsbnd2  32127  heibor1lem  32141  heiborlem1  32143  heiborlem10  32152  heibor  32153  riscer  32227  divrngidl  32261  prtlem17  32448  ax12eq  32512  ax12el  32513  ax12inda  32519  ax12v2-o  32520  osumcllem8N  33528  pexmidlem5N  33539  mapdrvallem2  35213  clcnvlem  36230  onfrALT  36915  chordthmALT  37330  ssnnf1octb  37470  choicefi  37481  inficc  37636  fsumnncl  37650  stoweidlem43  37904  stoweidlem48  37909  stoweidlem57  37918  stoweidlem60  37921  qndenserrnopn  38167  sge0cl  38223  nnfoctbdj  38294  ismeannd  38305  caragenunicl  38345  isomennd  38352  ovn0lem  38387  ovnsubaddlem2  38393  hspdifhsp  38438  hspmbllem3  38450  rlimdmafv  38679  upgredg  39228  usgr1v0e  39392  cplgr1v  39497  usgo1s0ALT  39802  usgo1s0  39807  mgmpropd  39828  c0snmgmhm  39967