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  4784  elpreqprb  4826  reusv2lem2  5346  ralxfr2d  5357  euotd  5469  wefrc  5626  wereu2  5629  releldmb  5903  relelrnb  5904  iss  6002  frpomin  6306  onfr  6364  dffv2  6937  dff3  7054  elunirn  7207  fsnex  7239  f1prex  7240  isomin  7293  isofrlem  7296  ovmpt4g  7515  soex  7873  f1oweALT  7926  op1steq  7987  fo2ndf  8073  frxp3  8103  mpoxopynvov0g  8166  reldmtpos  8186  rntpos  8191  frrlem10  8247  fprresex  8262  erdisj  8703  map0g  8834  resixpfo  8886  domdifsn  9000  xpdom3  9015  domunsncan  9017  enfixsn  9026  fodomr  9068  mapdom2  9088  mapdom3  9089  rexdif1en  9097  pssnn  9105  ssfiALT  9110  domfi  9125  sucdom2  9139  phplem2  9141  php3  9145  0sdom1dom  9158  sdom1  9162  1sdom2dom  9166  ac6sfi  9196  isfinite2  9210  domunfican  9234  fiint  9239  fodomfir  9240  fodomfib  9241  fodomfibOLD  9243  mapfien2  9324  marypha1lem  9348  ordiso  9433  hartogslem1  9459  brwdom2  9490  wdomtr  9492  brwdom3  9499  unwdomg  9501  xpwdomg  9502  unxpwdom2  9505  inf3lem2  9550  ttrclss  9641  dmttrcl  9642  rnttrcl  9643  ttrclselem2  9647  epfrs  9652  tcmin  9660  frmin  9673  cplem1  9813  pm54.43  9925  dfac8alem  9951  dfac8b  9953  dfac8clem  9954  ac10ct  9956  acni2  9968  acndom  9973  numwdom  9981  wdomfil  9983  wdomnumr  9986  iunfictbso  10036  dfac2b  10053  dfac9  10059  kmlem13  10085  djuinf  10111  fictb  10166  cfeq0  10178  cff1  10180  cfflb  10181  cofsmo  10191  cfsmolem  10192  coftr  10195  infpssr  10230  fin4en1  10231  fin23lem7  10238  isf34lem4  10299  axcc3  10360  domtriomlem  10364  axdc2lem  10370  axdc3lem2  10373  axdc3lem4  10375  axdc4lem  10377  ac6num  10401  ttukeylem6  10436  ttukeyg  10439  fodomb  10448  iundom2g  10462  alephreg  10505  fpwwe2lem10  10563  fpwwe2lem11  10564  canthp1  10577  pwfseq  10587  gruen  10735  grudomon  10740  gruina  10741  grur1  10743  ltexnq  10898  ltbtwnnq  10901  genpn0  10926  psslinpr  10954  prlem934  10956  ltaddpr  10957  ltexprlem2  10960  ltexprlem6  10964  ltexprlem7  10965  reclem2pr  10971  reclem4pr  10973  suplem1pr  10975  negn0  11578  sup2  12110  supaddc  12121  supmul1  12123  zsupss  12862  fiinfnf1o  14285  hasheqf1oi  14286  hashfun  14372  hashf1  14392  hash3tpexb  14429  rtrclreclem3  14995  rlimdm  15486  climcau  15606  caucvgb  15615  summolem2  15651  zsum  15653  sumz  15657  fsumf1o  15658  fsumss  15660  fsumcl2lem  15666  fsumadd  15675  fsummulc2  15719  fsumconst  15725  fsumrelem  15742  ntrivcvg  15832  prodmolem2  15870  zprod  15872  prod1  15879  fprodf1o  15881  fprodss  15883  fprodcl2lem  15885  fprodmul  15895  fproddiv  15896  fprodconst  15913  fprodn0  15914  ruclem13  16179  4sqlem12  16896  vdwapun  16914  vdwlem9  16929  vdwlem10  16930  ramz  16965  ramub1  16968  firest  17364  mremre  17535  isacs2  17588  iscatd2  17616  cicsym  17740  sscfn1  17753  sscfn2  17754  initoeu2  17952  mgmpropd  18588  gsumval2a  18622  symggen  19411  cyggex2  19838  gsumval3  19848  gsumzres  19850  gsumzcl2  19851  gsumzf1o  19853  gsumzaddlem  19862  gsumconst  19875  gsumzmhm  19878  gsumzoppg  19885  gsum2d2  19915  pgpfac1lem5  20022  ablfaclem3  20030  c0snmgmhm  20410  lss0cl  20910  lspsnat  21112  cnsubrg  21394  gsumfsum  21401  obslbs  21697  lmiclbs  21804  lmisfree  21809  mdetdiaglem  22554  mdet0  22562  eltg3  22918  tgtop  22929  tgidm  22936  ppttop  22963  toponmre  23049  tgrest  23115  neitr  23136  tgcn  23208  cmpsublem  23355  cmpsub  23356  iunconnlem  23383  unconn  23385  1stcfb  23401  2ndcctbss  23411  2ndcdisj  23412  1stcelcls  23417  1stccnp  23418  locfincmp  23482  comppfsc  23488  1stckgen  23510  ptuni2  23532  ptbasfi  23537  ptpjopn  23568  ptclsg  23571  ptcnp  23578  prdstopn  23584  txindis  23590  txtube  23596  txcmplem1  23597  txcmplem2  23598  xkococnlem  23615  txconn  23645  trfbas2  23799  filtop  23811  filconn  23839  filssufilg  23867  fmfnfm  23914  ufldom  23918  hauspwpwf1  23943  alexsubALTlem3  24005  alexsubALT  24007  ptcmplem2  24009  tmdgsum2  24052  tgptsmscld  24107  ustfilxp  24169  xbln0  24370  opnreen  24788  metdsre  24810  cnheibor  24922  phtpc01  24963  cfilfcls  25242  cmetcaulem  25256  iscmet3  25261  ovolctb  25459  ovoliunlem3  25473  ovoliunnul  25476  ovolicc2lem5  25490  ovolicc2  25491  dyadmbl  25569  vitali  25582  itg11  25660  bddmulibl  25808  perfdvf  25872  dvcnp2  25889  dvcnp2OLD  25890  dvlip  25966  dvne0  25984  fta1g  26143  fta1  26284  ulmcau  26372  pserulm  26399  wilthlem2  27047  dchrvmasumif  27482  rpvmasum2  27491  dchrisum0re  27492  dchrisum0lem3  27498  dchrisum0  27499  dchrmusum  27503  dchrvmasum  27504  noinfno  27698  nobdaymin  27761  ltslpss  27916  axcontlem10  29058  usgr1v0e  29411  wlkiswwlks  29961  wlkiswwlkupgr  29963  wlklnwwlkn  29969  wlklnwwlknupgr  29971  usgrwwlks2on  30043  umgrwwlks2on  30044  elwwlks2  30054  elwspths2spth  30055  clwlkclwwlklem3  30088  clwlkclwwlkfo  30096  frgr3vlem2  30361  spansncvi  31739  2ndresdju  32738  fnpreimac  32759  gsumwrd2dccatlem  33170  qsidomlem2  33545  reff  34016  locfinreflem  34017  cmpcref  34027  fmcncfil  34108  volmeas  34408  omssubadd  34477  bnj849  35100  r1filimi  35278  acycgrislfgr  35365  derangenlem  35384  cvmsss2  35487  cvmopnlem  35491  cvmfolem  35492  cvmliftmolem2  35495  cvmliftlem15  35511  cvmlift2lem10  35525  cvmlift3lem8  35539  satfdmlem  35581  sat1el2xp  35592  fmlasuc  35599  fundmpss  35980  fnessref  36570  refssfne  36571  neibastop2lem  36573  neibastop2  36574  fnemeet2  36580  fnejoin2  36582  tailfb  36590  knoppcnlem9  36720  isinf2  37657  pibt2  37669  wl-ax13lem1  37746  wl-sbcom2d  37813  matunitlindflem2  37865  poimirlem25  37893  poimirlem27  37895  heicant  37903  itg2addnclem  37919  sdclem1  37991  fdc  37993  istotbnd3  38019  sstotbnd2  38022  prdsbnd2  38043  heibor1lem  38057  heiborlem1  38059  heiborlem10  38068  heibor  38069  riscer  38236  divrngidl  38276  iss2  38592  eqvreldisj  38946  disjlem17  39150  prtlem17  39249  ax12eq  39314  ax12el  39315  ax12inda  39321  ax12v2-o  39322  osumcllem8N  40336  pexmidlem5N  40347  mapdrvallem2  42018  sn-sup2  42858  onexomgt  43595  onexoegt  43598  omabs2  43686  clcnvlem  43976  onfrALT  44902  chordthmALT  45285  relpmin  45305  relpfrlem  45306  modelaxreplem1  45331  wfac8prim  45355  snelmap  45439  ssnnf1octb  45550  choicefi  45555  mapss2  45560  difmap  45562  axccdom  45577  infxrlesupxr  45791  inficc  45891  fsumnncl  45929  stoweidlem43  46398  stoweidlem48  46403  stoweidlem57  46412  stoweidlem60  46415  qndenserrnopn  46653  issalnnd  46700  subsaliuncl  46713  sge0cl  46736  nnfoctbdj  46811  ismeannd  46822  caragenunicl  46879  isomennd  46886  ovn0lem  46920  ovnsubaddlem2  46926  hspdifhsp  46971  hspmbllem3  46983  smflimlem6  47131  smfpimbor1lem1  47153  smfpimcc  47163  smfsuplem2  47167  rlimdmafv  47534  dfatcolem  47612  rlimdmafv2  47615  grimuhgr  48244  grimcnv  48245  grimco  48246  uhgrimedgi  48247  isuspgrim0  48251  gricushgr  48274  gricsym  48278  uhgrimisgrgric  48288  clnbgrgrimlem  48290  clnbgrgrim  48291  grimedg  48292  grtriprop  48298  usgrgrtrirex  48307  isubgr3stgrlem3  48325  uspgrlim  48349  grlimprclnbgredg  48354  grlimgredgex  48357  grlimgrtri  48360  xpco2  49213  opnneilv  49265  thincciso  49809