Theorem exlimdv 1747

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

Syntax hints:   -> wi 4   E.wex 1635

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727

This theorem depends on definitions:  df-bi 187  df-ex 1636

This theorem is referenced by:  exlimdvv  1748  exlimddv  1749  axc9lem1  2030  nfeqf  2073  ax12v2  2111  sbcom2  2215  tpid3g  4089  sssn  4132  reusv2lem2  4598  ralxfr2d  4609  euotd  4693  wefrc  4819  wereu2  4822  releldmb  5060  relelrnb  5061  elres  5131  iss  5143  onfr  5451  dffv2  5924  dff3  6024  elunirn  6146  fsnex  6171  f1prex  6172  isomin  6218  isofrlem  6221  ovmpt4g  6408  soex  6729  f1oweALT  6770  op1steq  6828  fo2ndf  6893  mpt2xopynvov0g  6947  reldmtpos  6968  rntpos  6973  wfrlem12  7034  wfrlem17  7039  erdisj  7398  map0g  7498  resixpfo  7547  domdifsn  7640  xpdom3  7655  domunsncan  7657  enfixsn  7666  fodomr  7708  mapdom2  7728  mapdom3  7729  phplem4  7739  php3  7743  sucdom2  7753  pssnn  7775  ssfi  7777  domfi  7778  findcard2  7796  ac6sfi  7800  isfinite2  7814  xpfi  7827  domunfican  7829  fiint  7833  fodomfib  7836  mapfien2  7904  marypha1lem  7929  ordiso  7977  hartogslem1  8003  brwdom2  8035  wdomtr  8037  brwdom3  8044  unwdomg  8046  xpwdomg  8047  unxpwdom2  8050  inf3lem2  8081  epfrs  8196  tcmin  8206  cplem1  8341  pm54.43  8415  dfac8alem  8444  dfac8b  8446  dfac8clem  8447  ac10ct  8449  acni2  8461  acndom  8466  numwdom  8474  wdomfil  8476  wdomnumr  8479  iunfictbso  8529  dfac2  8545  dfac9  8550  kmlem13  8576  cdainf  8606  fictb  8659  cfeq0  8670  cff1  8672  cfflb  8673  cofsmo  8683  cfsmolem  8684  coftr  8687  infpssr  8722  fin4en1  8723  fin23lem7  8730  isf34lem4  8791  axcc3  8852  domtriomlem  8856  axdc2lem  8862  axdc3lem2  8865  axdc3lem4  8867  axdc4lem  8869  ac6num  8893  ttukeylem6  8928  ttukeyg  8931  fodomb  8938  iundom2g  8949  alephreg  8991  fpwwe2lem11  9050  fpwwe2lem12  9051  canthp1  9064  pwfseq  9074  gruen  9222  grudomon  9227  gruina  9228  grur1  9230  ltexnq  9385  ltbtwnnq  9388  genpn0  9413  psslinpr  9441  prlem934  9443  ltaddpr  9444  ltexprlem2  9447  ltexprlem6  9451  ltexprlem7  9452  reclem2pr  9458  reclem4pr  9460  suplem1pr  9462  sup2  10541  supmul1  10550  infmrcl  10564  negn0  11215  zsupss  11218  fiinfnf1o  12472  hashfun  12546  hashf1  12557  rtrclreclem3  13044  rlimdm  13525  climcau  13644  caucvgb  13653  summolem2  13689  zsum  13691  sumz  13695  fsumf1o  13696  fsumss  13698  fsumcl2lem  13704  fsumadd  13712  fsummulc2  13752  fsumconst  13758  fsumrelem  13774  ntrivcvg  13860  prodmolem2  13896  zprod  13898  prod1  13905  fprodf1o  13907  fprodss  13909  fprodcl2lem  13911  fprodmul  13919  fproddiv  13920  fprodconst  13936  fprodn0  13937  ruclem13  14186  4sqlem12  14685  vdwapun  14703  vdwlem9  14718  vdwlem10  14719  ramz  14754  ramub1  14757  firest  15049  mremre  15220  isacs2  15269  iscatd2  15297  sscfn1  15432  sscfn2  15433  gsumval2a  16232  symggen  16821  cyggex2  17225  gsumval3OLD  17234  gsumval3  17237  gsumzres  17240  gsumzcl2  17241  gsumzf1o  17243  gsumzresOLD  17244  gsumzclOLD  17245  gsumzf1oOLD  17246  gsumzaddlem  17260  gsumzaddlemOLD  17262  gsumconst  17279  gsumzmhm  17282  gsumzmhmOLD  17283  gsumzoppg  17292  gsumzoppgOLD  17293  gsum2d2  17325  pgpfac1lem5  17452  ablfaclem3  17460  lss0cl  17915  lspsnat  18113  cnsubrg  18800  gsumfsum  18806  obslbs  19061  lmiclbs  19166  lmisfree  19171  mdetdiaglem  19394  mdet0  19402  eltg3  19757  tgtop  19769  tgidm  19776  ppttop  19802  toponmre  19889  tgrest  19955  neitr  19976  tgcn  20048  cmpsublem  20194  cmpsub  20195  iunconlem  20222  uncon  20224  1stcfb  20240  2ndcctbss  20250  2ndcdisj  20251  1stcelcls  20256  1stccnp  20257  locfincmp  20321  comppfsc  20327  1stckgen  20349  ptuni2  20371  ptbasfi  20376  ptpjopn  20407  ptclsg  20410  ptcnp  20417  prdstopn  20423  txindis  20429  txtube  20435  txcmplem1  20436  txcmplem2  20437  xkococnlem  20454  txcon  20484  trfbas2  20638  filtop  20650  filcon  20678  filssufilg  20706  fmfnfm  20753  ufldom  20757  hauspwpwf1  20782  alexsubALTlem3  20843  alexsubALT  20845  ptcmplem2  20847  tmdgsum2  20889  tgptsmscld  20947  ustfilxp  21009  xbln0  21211  opnreen  21630  metdsre  21651  cnheibor  21749  phtpc01  21790  cfilfcls  22007  cmetcaulem  22021  iscmet3  22026  ovolctb  22195  ovoliunlem3  22209  ovoliunnul  22212  ovolicc2lem5  22226  ovolicc2  22227  dyadmbl  22303  vitali  22316  itg11  22392  bddmulibl  22539  perfdvf  22601  dvcnp2  22617  dvlip  22688  dvne0  22706  fta1g  22862  fta1  22998  ulmcau  23084  pserulm  23111  wilthlem2  23726  dchrvmasumif  24071  rpvmasum2  24080  dchrisum0re  24081  dchrisum0lem3  24087  dchrisum0  24088  dchrmusum  24092  dchrvmasum  24093  axcontlem10  24705  usgrafisindb1  24838  wlkiswwlk  25127  wlklniswwlkn  25130  clwlkisclwwlklem0  25217  clwlkfoclwwlk  25274  frgra3vlem2  25430  spansncvi  26997  reff  28308  locfinreflem  28309  cmpcref  28319  fmcncfil  28379  volmeas  28693  omssubadd  28761  bnj849  29323  derangenlem  29481  cvmsss2  29584  cvmopnlem  29588  cvmfolem  29589  cvmliftmolem2  29592  cvmliftlem15  29608  cvmlift2lem10  29622  cvmlift3lem8  29636  fundmpss  29993  frmin  30066  frrlem11  30112  nocvxmin  30164  fnessref  30598  refssfne  30599  neibastop2lem  30601  neibastop2  30602  fnemeet2  30608  fnejoin2  30610  tailfb  30618  bj-axc15v  30907  wl-sbcom2d  31391  wl-ax12v2  31407  supaddc  31426  heicant  31434  itg2addnclem  31452  sdclem1  31531  fdc  31533  istotbnd3  31562  sstotbnd2  31565  prdsbnd2  31586  heibor1lem  31600  heiborlem1  31602  heiborlem10  31611  heibor  31612  riscer  31686  divrngidl  31720  prtlem17  31912  ax12eq  31977  ax12el  31978  ax12inda  31984  ax12v2-o  31985  osumcllem8N  32993  pexmidlem5N  33004  mapdrvallem2  34678  mapfien2OLD  35417  onfrALT  36358  chordthmALT  36777  fsumnncl  36953  stoweidlem43  37206  stoweidlem48  37211  stoweidlem57  37220  stoweidlem60  37223  rlimdmafv  37643  usgo1s0ALT  38079  usgo1s0  38084  mgmpropd  38105  c0snmgmhm  38244