Theorem exlimdv 1935

Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2219. (Contributed by NM, 27-Apr-1994.) Remove dependencies on ax-6 1969, ax-7 2010. (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 1919	. 2 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
3		ax5e 1914	. 2 ⊢ (∃𝑥𝜒 → 𝜒)
4	2, 3	syl6 35	1 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))

Syntax hints:   → wi 4  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-ex 1782

This theorem is referenced by:  exlimdvv  1936  exlimddv  1937  ax13lem1  2379  ax13  2380  nfeqf  2386  axc15  2427  sssn  4770  elpreqprb  4812  reusv2lem2  5336  ralxfr2d  5347  euotd  5461  wefrc  5618  wereu2  5621  releldmb  5895  relelrnb  5896  iss  5994  frpomin  6298  onfr  6356  dffv2  6929  dff3  7046  elunirn  7199  fsnex  7231  f1prex  7232  isomin  7285  isofrlem  7288  ovmpt4g  7507  soex  7865  f1oweALT  7918  op1steq  7979  fo2ndf  8064  frxp3  8094  mpoxopynvov0g  8157  reldmtpos  8177  rntpos  8182  frrlem10  8238  fprresex  8253  erdisj  8694  map0g  8825  resixpfo  8877  domdifsn  8991  xpdom3  9006  domunsncan  9008  enfixsn  9017  fodomr  9059  mapdom2  9079  mapdom3  9080  rexdif1en  9088  pssnn  9096  ssfiALT  9101  domfi  9116  sucdom2  9130  phplem2  9132  php3  9136  0sdom1dom  9149  sdom1  9153  1sdom2dom  9157  ac6sfi  9187  isfinite2  9201  domunfican  9225  fiint  9230  fodomfir  9231  fodomfib  9232  fodomfibOLD  9234  mapfien2  9315  marypha1lem  9339  ordiso  9424  hartogslem1  9450  brwdom2  9481  wdomtr  9483  brwdom3  9490  unwdomg  9492  xpwdomg  9493  unxpwdom2  9496  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  20933  lspsnat  21135  cnsubrg  21417  gsumfsum  21424  obslbs  21720  lmiclbs  21827  lmisfree  21832  mdetdiaglem  22573  mdet0  22581  eltg3  22937  tgtop  22948  tgidm  22955  ppttop  22982  toponmre  23068  tgrest  23134  neitr  23155  tgcn  23227  cmpsublem  23374  cmpsub  23375  iunconnlem  23402  unconn  23404  1stcfb  23420  2ndcctbss  23430  2ndcdisj  23431  1stcelcls  23436  1stccnp  23437  locfincmp  23501  comppfsc  23507  1stckgen  23529  ptuni2  23551  ptbasfi  23556  ptpjopn  23587  ptclsg  23590  ptcnp  23597  prdstopn  23603  txindis  23609  txtube  23615  txcmplem1  23616  txcmplem2  23617  xkococnlem  23634  txconn  23664  trfbas2  23818  filtop  23830  filconn  23858  filssufilg  23886  fmfnfm  23933  ufldom  23937  hauspwpwf1  23962  alexsubALTlem3  24024  alexsubALT  24026  ptcmplem2  24028  tmdgsum2  24071  tgptsmscld  24126  ustfilxp  24188  xbln0  24389  opnreen  24807  metdsre  24829  cnheibor  24932  phtpc01  24973  cfilfcls  25251  cmetcaulem  25265  iscmet3  25270  ovolctb  25467  ovoliunlem3  25481  ovoliunnul  25484  ovolicc2lem5  25498  ovolicc2  25499  dyadmbl  25577  vitali  25590  itg11  25668  bddmulibl  25816  perfdvf  25880  dvcnp2  25897  dvlip  25970  dvne0  25988  fta1g  26145  fta1  26285  ulmcau  26373  pserulm  26400  wilthlem2  27046  dchrvmasumif  27480  rpvmasum2  27489  dchrisum0re  27490  dchrisum0lem3  27496  dchrisum0  27497  dchrmusum  27501  dchrvmasum  27502  noinfno  27696  nobdaymin  27759  ltslpss  27914  axcontlem10  29056  usgr1v0e  29409  wlkiswwlks  29959  wlkiswwlkupgr  29961  wlklnwwlkn  29967  wlklnwwlknupgr  29969  usgrwwlks2on  30041  umgrwwlks2on  30042  elwwlks2  30052  elwspths2spth  30053  clwlkclwwlklem3  30086  clwlkclwwlkfo  30094  frgr3vlem2  30359  spansncvi  31738  2ndresdju  32737  fnpreimac  32758  gsumwrd2dccatlem  33153  qsidomlem2  33528  reff  33999  locfinreflem  34000  cmpcref  34010  fmcncfil  34091  volmeas  34391  omssubadd  34460  bnj849  35083  r1filimi  35262  acycgrislfgr  35350  derangenlem  35369  cvmsss2  35472  cvmopnlem  35476  cvmfolem  35477  cvmliftmolem2  35480  cvmliftlem15  35496  cvmlift2lem10  35510  cvmlift3lem8  35524  satfdmlem  35566  sat1el2xp  35577  fmlasuc  35584  fundmpss  35965  fnessref  36555  refssfne  36556  neibastop2lem  36558  neibastop2  36559  fnemeet2  36565  fnejoin2  36567  tailfb  36575  axuntco  36677  dfttc4lem2  36727  knoppcnlem9  36777  isinf2  37735  pibt2  37747  wl-ax13lem1  37824  wl-sbcom2d  37900  matunitlindflem2  37952  poimirlem25  37980  poimirlem27  37982  heicant  37990  itg2addnclem  38006  sdclem1  38078  fdc  38080  istotbnd3  38106  sstotbnd2  38109  prdsbnd2  38130  heibor1lem  38144  heiborlem1  38146  heiborlem10  38155  heibor  38156  riscer  38323  divrngidl  38363  iss2  38679  eqvreldisj  39033  disjlem17  39237  prtlem17  39336  ax12eq  39401  ax12el  39402  ax12inda  39408  ax12v2-o  39409  osumcllem8N  40423  pexmidlem5N  40434  mapdrvallem2  42105  sn-sup2  42950  onexomgt  43687  onexoegt  43690  omabs2  43778  clcnvlem  44068  onfrALT  44994  chordthmALT  45377  relpmin  45397  relpfrlem  45398  modelaxreplem1  45423  wfac8prim  45447  snelmap  45531  ssnnf1octb  45642  choicefi  45647  mapss2  45652  difmap  45654  axccdom  45669  infxrlesupxr  45882  inficc  45982  fsumnncl  46020  stoweidlem43  46489  stoweidlem48  46494  stoweidlem57  46503  stoweidlem60  46506  qndenserrnopn  46744  issalnnd  46791  subsaliuncl  46804  sge0cl  46827  nnfoctbdj  46902  ismeannd  46913  caragenunicl  46970  isomennd  46977  ovn0lem  47011  ovnsubaddlem2  47017  hspdifhsp  47062  hspmbllem3  47074  smflimlem6  47222  smfpimbor1lem1  47244  smfpimcc  47254  smfsuplem2  47258  rlimdmafv  47637  dfatcolem  47715  rlimdmafv2  47718  grimuhgr  48375  grimcnv  48376  grimco  48377  uhgrimedgi  48378  isuspgrim0  48382  gricushgr  48405  gricsym  48409  uhgrimisgrgric  48419  clnbgrgrimlem  48421  clnbgrgrim  48422  grimedg  48423  grtriprop  48429  usgrgrtrirex  48438  isubgr3stgrlem3  48456  uspgrlim  48480  grlimprclnbgredg  48485  grlimgredgex  48488  grlimgrtri  48491  xpco2  49344  opnneilv  49396  thincciso  49940