Theorem exlimdv 1725

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

Syntax hints:   -> wi 4   E.wex 1613

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705

This theorem depends on definitions:  df-bi 185  df-ex 1614

This theorem is referenced by:  exlimdvv  1726  exlimddv  1727  axc9lem1  2002  nfeqf  2046  ax12v2  2084  sbcom2  2190  ax12eq  2272  ax12el  2273  ax12inda  2279  ax12v2-o  2280  tpid3g  4147  sssn  4190  reusv2lem2  4658  ralxfr2d  4672  euotd  4757  wefrc  4882  wereu2  4885  onfr  4926  releldmb  5247  relelrnb  5248  elres  5319  iss  5331  dffv2  5946  dff3  6045  elunirn  6164  isomin  6234  isofrlem  6237  ovmpt4g  6424  soex  6742  f1oweALT  6783  op1steq  6841  fo2ndf  6906  mpt2xopynvov0g  6960  reldmtpos  6981  rntpos  6986  erdisj  7377  map0g  7477  resixpfo  7526  domdifsn  7619  xpdom3  7634  domunsncan  7636  enfixsn  7645  fodomr  7687  mapdom2  7707  mapdom3  7708  phplem4  7718  php3  7722  sucdom2  7733  pssnn  7757  ssfi  7759  domfi  7760  findcard2  7778  ac6sfi  7782  isfinite2  7796  xpfi  7809  domunfican  7811  fiint  7815  fodomfib  7818  mapfien2  7886  marypha1lem  7911  ordiso  7959  hartogslem1  7985  brwdom2  8017  wdomtr  8019  brwdom3  8026  unwdomg  8028  xpwdomg  8029  unxpwdom2  8032  inf3lem2  8063  epfrs  8179  tcmin  8189  cplem1  8324  pm54.43  8398  dfac8alem  8427  dfac8b  8429  dfac8clem  8430  ac10ct  8432  acni2  8444  acndom  8449  numwdom  8457  wdomfil  8459  wdomnumr  8462  iunfictbso  8512  dfac2  8528  dfac9  8533  kmlem13  8559  cdainf  8589  fictb  8642  cfeq0  8653  cff1  8655  cfflb  8656  cofsmo  8666  cfsmolem  8667  coftr  8670  infpssr  8705  fin4en1  8706  fin23lem7  8713  isf34lem4  8774  axcc3  8835  domtriomlem  8839  axdc2lem  8845  axdc3lem2  8848  axdc3lem4  8850  axdc4lem  8852  ac6num  8876  ttukeylem6  8911  ttukeyg  8914  fodomb  8921  iundom2g  8932  alephreg  8974  fpwwe2lem11  9035  fpwwe2lem12  9036  canthp1  9049  pwfseq  9059  gruen  9207  grudomon  9212  gruina  9213  grur1  9215  ltexnq  9370  ltbtwnnq  9373  genpn0  9398  psslinpr  9426  prlem934  9428  ltaddpr  9429  ltexprlem2  9432  ltexprlem6  9436  ltexprlem7  9437  reclem2pr  9443  reclem4pr  9445  suplem1pr  9447  sup2  10519  supmul1  10528  infmrcl  10542  negn0  11193  zsupss  11196  fiinfnf1o  12426  hashfun  12499  hashf1  12510  rlimdm  13386  climcau  13505  caucvgb  13514  summolem2  13550  zsum  13552  sumz  13556  fsumf1o  13557  fsumss  13559  fsumcl2lem  13565  fsumadd  13573  fsummulc2  13611  fsumconst  13617  fsumrelem  13633  ntrivcvg  13718  prodmolem2  13754  zprod  13756  prod1  13763  fprodf1o  13765  fprodss  13767  fprodcl2lem  13769  fprodmul  13777  fproddiv  13778  fprodconst  13794  fprodn0  13795  ruclem13  13987  4sqlem12  14486  vdwapun  14504  vdwlem9  14519  vdwlem10  14520  ramz  14555  ramub1  14558  firest  14850  mremre  15021  isacs2  15070  iscatd2  15098  sscfn1  15233  sscfn2  15234  gsumval2a  16033  symggen  16622  cyggex2  17026  gsumval3OLD  17035  gsumval3  17038  gsumzres  17041  gsumzcl2  17042  gsumzf1o  17044  gsumzresOLD  17045  gsumzclOLD  17046  gsumzf1oOLD  17047  gsumzaddlem  17061  gsumzaddlemOLD  17063  gsumconst  17081  gsumzmhm  17084  gsumzmhmOLD  17085  gsumzoppg  17094  gsumzoppgOLD  17095  gsum2d2  17129  pgpfac1lem5  17257  ablfaclem3  17265  lss0cl  17720  lspsnat  17918  cnsubrg  18605  gsumfsum  18611  obslbs  18888  lmiclbs  18999  lmisfree  19004  mdetdiaglem  19227  mdet0  19235  eltg3  19590  tgtop  19602  tgidm  19609  ppttop  19635  toponmre  19721  tgrest  19787  neitr  19808  tgcn  19880  cmpsublem  20026  cmpsub  20027  iunconlem  20054  uncon  20056  1stcfb  20072  2ndcctbss  20082  2ndcdisj  20083  1stcelcls  20088  1stccnp  20089  locfincmp  20153  comppfsc  20159  1stckgen  20181  ptuni2  20203  ptbasfi  20208  ptpjopn  20239  ptclsg  20242  ptcnp  20249  prdstopn  20255  txindis  20261  txtube  20267  txcmplem1  20268  txcmplem2  20269  xkococnlem  20286  txcon  20316  trfbas2  20470  filtop  20482  filcon  20510  filssufilg  20538  fmfnfm  20585  ufldom  20589  hauspwpwf1  20614  alexsubALTlem3  20675  alexsubALT  20677  ptcmplem2  20679  tmdgsum2  20721  tgptsmscld  20779  ustfilxp  20841  xbln0  21043  opnreen  21462  metdsre  21483  cnheibor  21581  phtpc01  21622  cfilfcls  21839  cmetcaulem  21853  iscmet3  21858  ovolctb  22027  ovoliunlem3  22041  ovoliunnul  22044  ovolicc2lem5  22058  ovolicc2  22059  dyadmbl  22135  vitali  22148  itg11  22224  bddmulibl  22371  perfdvf  22433  dvcnp2  22449  dvlip  22520  dvne0  22538  fta1g  22694  fta1  22830  ulmcau  22916  pserulm  22943  wilthlem2  23469  dchrvmasumif  23814  rpvmasum2  23823  dchrisum0re  23824  dchrisum0lem3  23830  dchrisum0  23831  dchrmusum  23835  dchrvmasum  23836  axcontlem10  24403  usgrafisindb1  24536  wlkiswwlk  24825  wlklniswwlkn  24828  clwlkisclwwlklem0  24915  clwlkfoclwwlk  24972  frgra3vlem2  25128  spansncvi  26697  reff  28003  locfinreflem  28004  cmpcref  28014  fmcncfil  28074  volmeas  28376  omssubadd  28444  derangenlem  28812  cvmsss2  28916  cvmopnlem  28920  cvmfolem  28921  cvmliftmolem2  28924  cvmliftlem15  28940  cvmlift2lem10  28954  cvmlift3lem8  28968  rtrclreclem.trans  29287  fundmpss  29414  frmin  29539  wfrlem12  29571  frrlem11  29616  nocvxmin  29668  wl-sbcom2d  30216  supaddc  30246  heicant  30254  itg2addnclem  30271  fnessref  30380  refssfne  30381  neibastop2lem  30383  neibastop2  30384  fnemeet2  30390  fnejoin2  30392  tailfb  30400  sdclem1  30441  fdc  30443  istotbnd3  30472  sstotbnd2  30475  prdsbnd2  30496  heibor1lem  30510  heiborlem1  30512  heiborlem10  30521  heibor  30522  riscer  30596  divrngidl  30630  prtlem17  30822  mapfien2OLD  31246  fsumnncl  31775  stoweidlem43  32028  stoweidlem48  32033  stoweidlem57  32042  stoweidlem60  32045  rlimdmafv  32465  usgo1s0ALT  32699  usgo1s0  32704  mgmpropd  32725  c0snmgmhm  32864  onfrALT  33464  chordthmALT  33876  bnj849  34126  bj-axc15v  34473  osumcllem8N  35830  pexmidlem5N  35841  mapdrvallem2  37515