Theorem exlimdv 1861

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

Syntax hints:   -> wi 4   E.wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839

This theorem depends on definitions:  df-bi 197  df-ex 1705

This theorem is referenced by:  exlimdvv  1862  exlimddv  1863  ax13lem1  2248  ax13  2249  nfeqf  2301  axc15  2303  ax12v2OLD  2342  sbcom2  2445  tpid3gOLD  4306  sssn  4358  elpreqprb  4397  reusv2lem2  4869  reusv2lem2OLD  4870  ralxfr2d  4882  euotd  4975  wefrc  5108  wereu2  5111  releldmb  5360  relelrnb  5361  elres  5435  iss  5447  onfr  5763  dffv2  6271  dff3  6372  elunirn  6509  fsnex  6538  f1prex  6539  isomin  6587  isofrlem  6590  ovmpt4g  6783  soex  7109  f1oweALT  7152  op1steq  7210  fo2ndf  7284  mpt2xopynvov0g  7340  reldmtpos  7360  rntpos  7365  wfrlem12  7426  wfrlem17  7431  erdisj  7794  map0g  7897  resixpfo  7946  domdifsn  8043  xpdom3  8058  domunsncan  8060  enfixsn  8069  fodomr  8111  mapdom2  8131  mapdom3  8132  phplem4  8142  php3  8146  sucdom2  8156  pssnn  8178  ssfi  8180  domfi  8181  findcard2  8200  ac6sfi  8204  isfinite2  8218  xpfi  8231  domunfican  8233  fiint  8237  fodomfib  8240  mapfien2  8314  marypha1lem  8339  ordiso  8421  hartogslem1  8447  brwdom2  8478  wdomtr  8480  brwdom3  8487  unwdomg  8489  xpwdomg  8490  unxpwdom2  8493  inf3lem2  8526  epfrs  8607  tcmin  8617  cplem1  8752  pm54.43  8826  dfac8alem  8852  dfac8b  8854  dfac8clem  8855  ac10ct  8857  acni2  8869  acndom  8874  numwdom  8882  wdomfil  8884  wdomnumr  8887  iunfictbso  8937  dfac2  8953  dfac9  8958  kmlem13  8984  cdainf  9014  fictb  9067  cfeq0  9078  cff1  9080  cfflb  9081  cofsmo  9091  cfsmolem  9092  coftr  9095  infpssr  9130  fin4en1  9131  fin23lem7  9138  isf34lem4  9199  axcc3  9260  domtriomlem  9264  axdc2lem  9270  axdc3lem2  9273  axdc3lem4  9275  axdc4lem  9277  ac6num  9301  ttukeylem6  9336  ttukeyg  9339  fodomb  9348  iundom2g  9362  alephreg  9404  fpwwe2lem11  9462  fpwwe2lem12  9463  canthp1  9476  pwfseq  9486  gruen  9634  grudomon  9639  gruina  9640  grur1  9642  ltexnq  9797  ltbtwnnq  9800  genpn0  9825  psslinpr  9853  prlem934  9855  ltaddpr  9856  ltexprlem2  9859  ltexprlem6  9863  ltexprlem7  9864  reclem2pr  9870  reclem4pr  9872  suplem1pr  9874  negn0  10459  sup2  10979  supaddc  10990  supmul1  10992  zsupss  11777  fiinfnf1o  13138  hasheqf1oi  13140  hashfun  13224  hashf1  13241  rtrclreclem3  13800  rlimdm  14282  climcau  14401  caucvgb  14410  summolem2  14447  zsum  14449  sumz  14453  fsumf1o  14454  fsumss  14456  fsumcl2lem  14462  fsumadd  14470  fsummulc2  14516  fsumconst  14522  fsumrelem  14539  ntrivcvg  14629  prodmolem2  14665  zprod  14667  prod1  14674  fprodf1o  14676  fprodss  14678  fprodcl2lem  14680  fprodmul  14690  fproddiv  14691  fprodconst  14708  fprodn0  14709  ruclem13  14971  4sqlem12  15660  vdwapun  15678  vdwlem9  15693  vdwlem10  15694  ramz  15729  ramub1  15732  firest  16093  mremre  16264  isacs2  16314  iscatd2  16342  sscfn1  16477  sscfn2  16478  gsumval2a  17279  symggen  17890  cyggex2  18298  gsumval3  18308  gsumzres  18310  gsumzcl2  18311  gsumzf1o  18313  gsumzaddlem  18321  gsumconst  18334  gsumzmhm  18337  gsumzoppg  18344  gsum2d2  18373  pgpfac1lem5  18478  ablfaclem3  18486  lss0cl  18947  lspsnat  19145  cnsubrg  19806  gsumfsum  19813  obslbs  20074  lmiclbs  20176  lmisfree  20181  mdetdiaglem  20404  mdet0  20412  eltg3  20766  tgtop  20777  tgidm  20784  ppttop  20811  toponmre  20897  tgrest  20963  neitr  20984  tgcn  21056  cmpsublem  21202  cmpsub  21203  iunconnlem  21230  unconn  21232  1stcfb  21248  2ndcctbss  21258  2ndcdisj  21259  1stcelcls  21264  1stccnp  21265  locfincmp  21329  comppfsc  21335  1stckgen  21357  ptuni2  21379  ptbasfi  21384  ptpjopn  21415  ptclsg  21418  ptcnp  21425  prdstopn  21431  txindis  21437  txtube  21443  txcmplem1  21444  txcmplem2  21445  xkococnlem  21462  txconn  21492  trfbas2  21647  filtop  21659  filconn  21687  filssufilg  21715  fmfnfm  21762  ufldom  21766  hauspwpwf1  21791  alexsubALTlem3  21853  alexsubALT  21855  ptcmplem2  21857  tmdgsum2  21900  tgptsmscld  21954  ustfilxp  22016  xbln0  22219  opnreen  22634  metdsre  22656  cnheibor  22754  phtpc01  22796  cfilfcls  23072  cmetcaulem  23086  iscmet3  23091  ovolctb  23258  ovoliunlem3  23272  ovoliunnul  23275  ovolicc2lem5  23289  ovolicc2  23290  dyadmbl  23368  vitali  23382  itg11  23458  bddmulibl  23605  perfdvf  23667  dvcnp2  23683  dvlip  23756  dvne0  23774  fta1g  23927  fta1  24063  ulmcau  24149  pserulm  24176  wilthlem2  24795  dchrvmasumif  25192  rpvmasum2  25201  dchrisum0re  25202  dchrisum0lem3  25208  dchrisum0  25209  dchrmusum  25213  dchrvmasum  25214  axcontlem10  25853  usgr1v0e  26218  wlkiswwlks  26762  wlkiswwlkupgr  26764  wlklnwwlkn  26770  wlklnwwlknupgr  26772  umgrwwlks2on  26850  elwwlks2  26861  elwspths2spth  26862  clwlkclwwlklem3  26902  clwlksfoclwwlk  26963  frgr3vlem2  27138  spansncvi  28511  reff  29906  locfinreflem  29907  cmpcref  29917  fmcncfil  29977  volmeas  30294  omssubadd  30362  bnj849  30995  derangenlem  31153  cvmsss2  31256  cvmopnlem  31260  cvmfolem  31261  cvmliftmolem2  31264  cvmliftlem15  31280  cvmlift2lem10  31294  cvmlift3lem8  31308  fundmpss  31664  frmin  31739  frrlem11  31792  nocvxmin  31894  fnessref  32352  refssfne  32353  neibastop2lem  32355  neibastop2  32356  fnemeet2  32362  fnejoin2  32364  tailfb  32372  knoppcnlem9  32491  wl-ax13lem1  33287  wl-sbcom2d  33344  matunitlindflem2  33406  poimirlem25  33434  poimirlem27  33436  heicant  33444  itg2addnclem  33461  sdclem1  33539  fdc  33541  istotbnd3  33570  sstotbnd2  33573  prdsbnd2  33594  heibor1lem  33608  heiborlem1  33610  heiborlem10  33619  heibor  33620  riscer  33787  divrngidl  33827  iss2  34112  prtlem17  34161  ax12eq  34226  ax12el  34227  ax12inda  34233  ax12v2-o  34234  osumcllem8N  35249  pexmidlem5N  35260  mapdrvallem2  36934  clcnvlem  37930  onfrALT  38764  chordthmALT  39169  snelmap  39254  ssnnf1octb  39382  choicefi  39392  mapss2  39397  difmap  39399  axccdom  39416  infxrlesupxr  39663  inficc  39761  fsumnncl  39803  stoweidlem43  40260  stoweidlem48  40265  stoweidlem57  40274  stoweidlem60  40277  qndenserrnopn  40518  issalnnd  40563  subsaliuncl  40576  sge0cl  40598  nnfoctbdj  40673  ismeannd  40684  caragenunicl  40738  isomennd  40745  ovn0lem  40779  ovnsubaddlem2  40785  hspdifhsp  40830  hspmbllem3  40842  smflimlem6  40984  smfpimbor1lem1  41005  smfpimcc  41014  smfsuplem2  41018  rlimdmafv  41257  mgmpropd  41775  c0snmgmhm  41914