Theorem exlimdv 1787

Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2013. (Contributed by NM, 27-Apr-1994.) Remove dependencies on ax-6 1813, ax-7 1859. (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 1772	. 2 |- ( ph -> ( E. x ps -> E. x ch ) )
3		ax5e 1768	. 2 |- ( E. x ch -> ch )
4	2, 3	syl6 33	1 |- ( ph -> ( E. x ps -> ch ) )

Syntax hints:   -> wi 4   E.wex 1671

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766

This theorem depends on definitions:  df-bi 190  df-ex 1672

This theorem is referenced by:  exlimdvv  1788  exlimddv  1789  axc9lem1  2106  nfeqf  2152  axc15  2153  ax12v2OLD  2191  sbcom2  2294  tpid3g  4078  sssn  4122  elpreqprb  4154  reusv2lem2  4603  ralxfr2d  4614  euotd  4702  wefrc  4833  wereu2  4836  releldmb  5075  relelrnb  5076  elres  5146  iss  5158  onfr  5469  dffv2  5953  dff3  6050  elunirn  6174  fsnex  6199  f1prex  6200  isomin  6246  isofrlem  6249  ovmpt4g  6438  soex  6755  f1oweALT  6796  op1steq  6854  fo2ndf  6922  mpt2xopynvov0g  6979  reldmtpos  6999  rntpos  7004  wfrlem12  7065  wfrlem17  7070  erdisj  7429  map0g  7529  resixpfo  7578  domdifsn  7673  xpdom3  7688  domunsncan  7690  enfixsn  7699  fodomr  7741  mapdom2  7761  mapdom3  7762  phplem4  7772  php3  7776  sucdom2  7786  pssnn  7808  ssfi  7810  domfi  7811  findcard2  7829  ac6sfi  7833  isfinite2  7847  xpfi  7860  domunfican  7862  fiint  7866  fodomfib  7869  mapfien2  7940  marypha1lem  7965  ordiso  8049  hartogslem1  8075  brwdom2  8106  wdomtr  8108  brwdom3  8115  unwdomg  8117  xpwdomg  8118  unxpwdom2  8121  inf3lem2  8152  epfrs  8233  tcmin  8243  cplem1  8378  pm54.43  8452  dfac8alem  8478  dfac8b  8480  dfac8clem  8481  ac10ct  8483  acni2  8495  acndom  8500  numwdom  8508  wdomfil  8510  wdomnumr  8513  iunfictbso  8563  dfac2  8579  dfac9  8584  kmlem13  8610  cdainf  8640  fictb  8693  cfeq0  8704  cff1  8706  cfflb  8707  cofsmo  8717  cfsmolem  8718  coftr  8721  infpssr  8756  fin4en1  8757  fin23lem7  8764  isf34lem4  8825  axcc3  8886  domtriomlem  8890  axdc2lem  8896  axdc3lem2  8899  axdc3lem4  8901  axdc4lem  8903  ac6num  8927  ttukeylem6  8962  ttukeyg  8965  fodomb  8972  iundom2g  8983  alephreg  9025  fpwwe2lem11  9083  fpwwe2lem12  9084  canthp1  9097  pwfseq  9107  gruen  9255  grudomon  9260  gruina  9261  grur1  9263  ltexnq  9418  ltbtwnnq  9421  genpn0  9446  psslinpr  9474  prlem934  9476  ltaddpr  9477  ltexprlem2  9480  ltexprlem6  9484  ltexprlem7  9485  reclem2pr  9491  reclem4pr  9493  suplem1pr  9495  negn0  10069  sup2  10587  supaddc  10596  supmul1  10598  infmrclOLD  10615  zsupss  11276  fiinfnf1o  12571  hashfun  12650  hashf1  12661  rtrclreclem3  13200  rlimdm  13692  climcau  13811  caucvgb  13823  summolem2  13859  zsum  13861  sumz  13865  fsumf1o  13866  fsumss  13868  fsumcl2lem  13874  fsumadd  13882  fsummulc2  13922  fsumconst  13928  fsumrelem  13944  ntrivcvg  14030  prodmolem2  14066  zprod  14068  prod1  14075  fprodf1o  14077  fprodss  14079  fprodcl2lem  14081  fprodmul  14091  fproddiv  14092  fprodconst  14109  fprodn0  14110  ruclem13  14371  4sqlem12  14979  vdwapun  15003  vdwlem9  15018  vdwlem10  15019  ramz  15062  ramub1  15065  firest  15409  mremre  15588  isacs2  15637  iscatd2  15665  sscfn1  15800  sscfn2  15801  gsumval2a  16600  symggen  17189  cyggex2  17609  gsumval3  17619  gsumzres  17621  gsumzcl2  17622  gsumzf1o  17624  gsumzaddlem  17632  gsumconst  17645  gsumzmhm  17648  gsumzoppg  17655  gsum2d2  17684  pgpfac1lem5  17790  ablfaclem3  17798  lss0cl  18248  lspsnat  18446  cnsubrg  19105  gsumfsum  19111  obslbs  19370  lmiclbs  19472  lmisfree  19477  mdetdiaglem  19700  mdet0  19708  eltg3  20054  tgtop  20066  tgidm  20073  ppttop  20099  toponmre  20186  tgrest  20252  neitr  20273  tgcn  20345  cmpsublem  20491  cmpsub  20492  iunconlem  20519  uncon  20521  1stcfb  20537  2ndcctbss  20547  2ndcdisj  20548  1stcelcls  20553  1stccnp  20554  locfincmp  20618  comppfsc  20624  1stckgen  20646  ptuni2  20668  ptbasfi  20673  ptpjopn  20704  ptclsg  20707  ptcnp  20714  prdstopn  20720  txindis  20726  txtube  20732  txcmplem1  20733  txcmplem2  20734  xkococnlem  20751  txcon  20781  trfbas2  20936  filtop  20948  filcon  20976  filssufilg  21004  fmfnfm  21051  ufldom  21055  hauspwpwf1  21080  alexsubALTlem3  21142  alexsubALT  21144  ptcmplem2  21146  tmdgsum2  21189  tgptsmscld  21243  ustfilxp  21305  xbln0  21507  opnreen  21927  metdsre  21948  metdsreOLD  21963  cnheibor  22061  phtpc01  22105  cfilfcls  22322  cmetcaulem  22336  iscmet3  22341  ovolctb  22521  ovoliunlem3  22535  ovoliunnul  22538  ovolicc2lem5  22553  ovolicc2  22554  dyadmbl  22637  vitali  22650  itg11  22728  bddmulibl  22875  perfdvf  22937  dvcnp2  22953  dvlip  23024  dvne0  23042  fta1g  23197  fta1  23340  ulmcau  23429  pserulm  23456  wilthlem2  24073  dchrvmasumif  24420  rpvmasum2  24429  dchrisum0re  24430  dchrisum0lem3  24436  dchrisum0  24437  dchrmusum  24441  dchrvmasum  24442  axcontlem10  25082  usgrafisindb1  25216  wlkiswwlk  25505  wlklniswwlkn  25508  clwlkisclwwlklem0  25595  clwlkfoclwwlk  25652  frgra3vlem2  25808  spansncvi  27386  reff  28740  locfinreflem  28741  cmpcref  28751  fmcncfil  28811  volmeas  29127  omssubadd  29201  omssubaddOLD  29205  bnj849  29808  derangenlem  29966  cvmsss2  30069  cvmopnlem  30073  cvmfolem  30074  cvmliftmolem2  30077  cvmliftlem15  30093  cvmlift2lem10  30107  cvmlift3lem8  30121  fundmpss  30478  frmin  30551  frrlem11  30597  nocvxmin  30651  fnessref  31084  refssfne  31085  neibastop2lem  31087  neibastop2  31088  fnemeet2  31094  fnejoin2  31096  tailfb  31104  bj-axc15v  31428  wl-sbcom2d  31961  poimirlem25  32029  poimirlem27  32031  heicant  32039  itg2addnclem  32057  sdclem1  32136  fdc  32138  istotbnd3  32167  sstotbnd2  32170  prdsbnd2  32191  heibor1lem  32205  heiborlem1  32207  heiborlem10  32216  heibor  32217  riscer  32291  divrngidl  32325  prtlem17  32512  ax12eq  32576  ax12el  32577  ax12inda  32583  ax12v2-o  32584  osumcllem8N  33599  pexmidlem5N  33610  mapdrvallem2  35284  clcnvlem  36301  onfrALT  36985  chordthmALT  37393  snelmap  37489  ssnnf1octb  37541  choicefi  37552  mapss2  37557  difmap  37559  inficc  37732  fsumnncl  37746  stoweidlem43  38016  stoweidlem48  38021  stoweidlem57  38030  stoweidlem60  38033  qndenserrnopn  38279  issalnnd  38316  sge0cl  38337  nnfoctbdj  38410  ismeannd  38421  caragenunicl  38464  isomennd  38471  ovn0lem  38505  ovnsubaddlem2  38511  hspdifhsp  38556  hspmbllem3  38568  rlimdmafv  38824  upgredg  39389  usgr1v0e  39556  usgo1s0ALT  40257  usgo1s0  40262  mgmpropd  40283  c0snmgmhm  40422