Theorem exlimdv 1940

Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2223. (Contributed by NM, 27-Apr-1994.) Remove dependencies on ax-6 1974, ax-7 2015. (Revised by Wolf Lammen, 4-Dec-2017.)

Hypothesis

Ref	Expression
exlimdv.1	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
exlimdv	⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))

Distinct variable groups:   𝜒,𝑥   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem exlimdv

Step	Hyp	Ref	Expression
1		exlimdv.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	eximdv 1924	. 2 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
3		ax5e 1919	. 2 ⊢ (∃𝑥𝜒 → 𝜒)
4	2, 3	syl6 35	1 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))

Syntax hints:   → wi 4  ∃wex 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  exlimdvv  1941  exlimddv  1942  ax13lem1  2382  ax13  2383  nfeqf  2389  axc15  2430  sssn  4757  elpreqprb  4799  reusv2lem2  5328  ralxfr2d  5339  euotd  5454  wefrc  5612  wereu2  5615  releldmb  5888  relelrnb  5889  iss  5987  frpomin  6291  onfr  6349  dffv2  6922  dff3  7041  elunirn  7195  fsnex  7227  f1prex  7228  isomin  7281  isofrlem  7284  ovmpt4g  7503  soex  7861  f1oweALT  7914  op1steq  7975  fo2ndf  8060  frxp3  8091  mpoxopynvov0g  8154  reldmtpos  8174  rntpos  8179  frrlem10  8235  fprresex  8250  erdisj  8691  map0g  8822  resixpfo  8874  domdifsn  8988  xpdom3  9003  domunsncan  9005  enfixsn  9014  fodomr  9056  mapdom2  9076  mapdom3  9077  rexdif1en  9085  pssnn  9093  ssfiALT  9098  domfi  9113  sucdom2  9127  phplem2  9129  php3  9133  0sdom1dom  9146  sdom1  9150  1sdom2dom  9154  ac6sfi  9184  isfinite2  9198  domunfican  9222  fiint  9227  fodomfir  9228  fodomfib  9229  fodomfibOLD  9231  mapfien2  9312  marypha1lem  9336  ordiso  9421  hartogslem1  9447  brwdom2  9478  wdomtr  9480  brwdom3  9487  unwdomg  9489  xpwdomg  9490  unxpwdom2  9493  inf3lem2  9541  ttrclss  9632  dmttrcl  9633  rnttrcl  9634  ttrclselem2  9638  epfrs  9643  tcmin  9651  frmin  9664  cplem1  9804  pm54.43  9916  dfac8alem  9942  dfac8b  9944  dfac8clem  9945  ac10ct  9947  acni2  9959  acndom  9964  numwdom  9972  wdomfil  9974  wdomnumr  9977  iunfictbso  10027  dfac2b  10044  dfac9  10050  kmlem13  10076  djuinf  10102  fictb  10157  cfeq0  10169  cff1  10171  cfflb  10172  cofsmo  10182  cfsmolem  10183  coftr  10186  infpssr  10221  fin4en1  10222  fin23lem7  10229  isf34lem4  10290  axcc3  10351  domtriomlem  10355  axdc2lem  10361  axdc3lem2  10364  axdc3lem4  10366  axdc4lem  10368  ac6num  10392  ttukeylem6  10427  ttukeyg  10430  fodomb  10439  iundom2g  10453  alephreg  10496  fpwwe2lem10  10554  fpwwe2lem11  10555  canthp1  10568  pwfseq  10578  gruen  10726  grudomon  10731  gruina  10732  grur1  10734  ltexnq  10889  ltbtwnnq  10892  genpn0  10917  psslinpr  10945  prlem934  10947  ltaddpr  10948  ltexprlem2  10951  ltexprlem6  10955  ltexprlem7  10956  reclem2pr  10962  reclem4pr  10964  suplem1pr  10966  negn0  11570  sup2  12103  supaddc  12114  supmul1  12116  zsupss  12878  fiinfnf1o  14303  hasheqf1oi  14304  hashfun  14390  hashf1  14410  hash3tpexb  14447  rtrclreclem3  15013  rlimdm  15504  climcau  15624  caucvgb  15633  summolem2  15669  zsum  15671  sumz  15675  fsumf1o  15676  fsumss  15678  fsumcl2lem  15684  fsumadd  15693  fsummulc2  15737  fsumconst  15743  fsumrelem  15761  ntrivcvg  15853  prodmolem2  15891  zprod  15893  prod1  15900  fprodf1o  15902  fprodss  15904  fprodcl2lem  15906  fprodmul  15916  fproddiv  15917  fprodconst  15934  fprodn0  15935  ruclem13  16200  4sqlem12  16918  vdwapun  16936  vdwlem9  16951  vdwlem10  16952  ramz  16987  ramub1  16990  firest  17386  mremre  17557  isacs2  17610  iscatd2  17638  cicsym  17762  sscfn1  17775  sscfn2  17776  initoeu2  17974  mgmpropd  18610  gsumval2a  18644  symggen  19436  cyggex2  19863  gsumval3  19873  gsumzres  19875  gsumzcl2  19876  gsumzf1o  19878  gsumzaddlem  19887  gsumconst  19900  gsumzmhm  19903  gsumzoppg  19910  gsum2d2  19940  pgpfac1lem5  20047  ablfaclem3  20055  c0snmgmhm  20433  lss0cl  20937  lspsnat  21138  cnsubrg  21402  gsumfsum  21409  obslbs  21705  lmiclbs  21812  lmisfree  21817  mdetdiaglem  22581  mdet0  22589  eltg3  22945  tgtop  22956  tgidm  22963  ppttop  22990  toponmre  23076  tgrest  23142  neitr  23163  tgcn  23235  cmpsublem  23382  cmpsub  23383  iunconnlem  23410  unconn  23412  1stcfb  23428  2ndcctbss  23438  2ndcdisj  23439  1stcelcls  23444  1stccnp  23445  locfincmp  23509  comppfsc  23515  1stckgen  23537  ptuni2  23559  ptbasfi  23564  ptpjopn  23595  ptclsg  23598  ptcnp  23605  prdstopn  23611  txindis  23617  txtube  23623  txcmplem1  23624  txcmplem2  23625  xkococnlem  23642  txconn  23672  trfbas2  23826  filtop  23838  filconn  23866  filssufilg  23894  fmfnfm  23941  ufldom  23945  hauspwpwf1  23970  alexsubALTlem3  24032  alexsubALT  24034  ptcmplem2  24036  tmdgsum2  24079  tgptsmscld  24134  ustfilxp  24196  xbln0  24397  opnreen  24815  metdsre  24837  cnheibor  24940  phtpc01  24981  cfilfcls  25259  cmetcaulem  25273  iscmet3  25278  ovolctb  25475  ovoliunlem3  25489  ovoliunnul  25492  ovolicc2lem5  25506  ovolicc2  25507  dyadmbl  25585  vitali  25598  itg11  25676  bddmulibl  25824  perfdvf  25888  dvcnp2  25905  dvlip  25978  dvne0  25996  fta1g  26153  fta1  26292  ulmcau  26378  pserulm  26405  wilthlem2  27050  dchrvmasumif  27484  rpvmasum2  27493  dchrisum0re  27494  dchrisum0lem3  27500  dchrisum0  27501  dchrmusum  27505  dchrvmasum  27506  noinfno  27700  nobdaymin  27763  ltslpss  27918  axcontlem10  29060  usgr1v0e  29413  wlkiswwlks  29962  wlkiswwlkupgr  29964  wlklnwwlkn  29970  wlklnwwlknupgr  29972  usgrwwlks2on  30044  umgrwwlks2on  30045  elwwlks2  30055  elwspths2spth  30056  clwlkclwwlklem3  30089  clwlkclwwlkfo  30097  frgr3vlem2  30362  spansncvi  31741  2ndresdju  32741  fnpreimac  32762  gsumwrd2dccatlem  33158  qsidomlem2  33536  reff  34023  locfinreflem  34024  cmpcref  34034  fmcncfil  34115  volmeas  34415  omssubadd  34484  bnj849  35107  r1filimi  35284  acycgrislfgr  35380  derangenlem  35399  cvmsss2  35502  cvmopnlem  35506  cvmfolem  35507  cvmliftmolem2  35510  cvmliftlem15  35526  cvmlift2lem10  35540  cvmlift3lem8  35554  satfdmlem  35596  sat1el2xp  35607  fmlasuc  35614  fundmpss  35995  fnessref  36585  refssfne  36586  neibastop2lem  36588  neibastop2  36589  fnemeet2  36595  fnejoin2  36597  tailfb  36605  axuntco  36707  dfttc4lem2  36757  knoppcnlem9  36807  isinf2  37767  pibt2  37779  wl-ax13lem1  37856  wl-sbcom2d  37932  matunitlindflem2  37984  poimirlem25  38012  poimirlem27  38014  heicant  38022  itg2addnclem  38038  sdclem1  38110  fdc  38112  istotbnd3  38138  sstotbnd2  38141  prdsbnd2  38162  heibor1lem  38176  heiborlem1  38178  heiborlem10  38187  heibor  38188  riscer  38355  divrngidl  38395  iss2  38711  eqvreldisj  39065  disjlem17  39269  prtlem17  39368  ax12eq  39433  ax12el  39434  ax12inda  39440  ax12v2-o  39441  osumcllem8N  40455  pexmidlem5N  40466  mapdrvallem2  42137  sn-sup2  42981  onexomgt  43686  onexoegt  43689  omabs2  43777  clcnvlem  44067  onfrALT  44993  chordthmALT  45376  relpmin  45396  relpfrlem  45397  modelaxreplem1  45422  wfac8prim  45446  snelmap  45530  ssnnf1octb  45641  choicefi  45646  mapss2  45651  difmap  45652  axccdom  45667  infxrlesupxr  45879  inficc  45979  fsumnncl  46017  stoweidlem43  46486  stoweidlem48  46491  stoweidlem57  46500  stoweidlem60  46503  qndenserrnopn  46741  issalnnd  46788  subsaliuncl  46801  sge0cl  46824  nnfoctbdj  46899  ismeannd  46910  caragenunicl  46967  isomennd  46974  ovn0lem  47008  ovnsubaddlem2  47014  hspdifhsp  47059  hspmbllem3  47071  smflimlem6  47219  smfpimbor1lem1  47241  smfpimcc  47251  smfsuplem2  47255  rlimdmafv  47640  dfatcolem  47718  rlimdmafv2  47721  grimuhgr  48378  grimcnv  48379  grimco  48380  uhgrimedgi  48381  isuspgrim0  48385  gricushgr  48408  gricsym  48412  uhgrimisgrgric  48422  clnbgrgrimlem  48424  clnbgrgrim  48425  grimedg  48426  grtriprop  48432  usgrgrtrirex  48441  isubgr3stgrlem3  48459  uspgrlim  48483  grlimprclnbgredg  48488  grlimgredgex  48491  grlimgrtri  48494  xpco2  49347  opnneilv  49399  thincciso  49943