Theorem exlimdv 1934

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

Syntax hints:   → wi 4  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  exlimdvv  1935  exlimddv  1936  ax13lem1  2374  ax13  2375  nfeqf  2381  axc15  2422  sssn  4773  elpreqprb  4815  reusv2lem2  5332  ralxfr2d  5343  euotd  5448  wefrc  5605  wereu2  5608  releldmb  5881  relelrnb  5882  iss  5979  frpomin  6282  onfr  6340  dffv2  6912  dff3  7028  elunirn  7180  fsnex  7212  f1prex  7213  isomin  7266  isofrlem  7269  ovmpt4g  7488  soex  7846  f1oweALT  7899  op1steq  7960  fo2ndf  8046  frxp3  8076  mpoxopynvov0g  8139  reldmtpos  8159  rntpos  8164  frrlem10  8220  fprresex  8235  erdisj  8674  map0g  8803  resixpfo  8855  domdifsn  8968  xpdom3  8983  domunsncan  8985  enfixsn  8994  fodomr  9036  mapdom2  9056  mapdom3  9057  rexdif1en  9065  pssnn  9073  ssfiALT  9078  domfi  9093  sucdom2  9107  phplem2  9109  php3  9113  0sdom1dom  9125  sdom1  9129  1sdom2dom  9133  ac6sfi  9163  isfinite2  9177  domunfican  9201  fiint  9206  fodomfir  9207  fodomfib  9208  fodomfibOLD  9210  mapfien2  9288  marypha1lem  9312  ordiso  9397  hartogslem1  9423  brwdom2  9454  wdomtr  9456  brwdom3  9463  unwdomg  9465  xpwdomg  9466  unxpwdom2  9469  inf3lem2  9514  ttrclss  9605  dmttrcl  9606  rnttrcl  9607  ttrclselem2  9611  epfrs  9616  tcmin  9624  frmin  9637  cplem1  9777  pm54.43  9889  dfac8alem  9915  dfac8b  9917  dfac8clem  9918  ac10ct  9920  acni2  9932  acndom  9937  numwdom  9945  wdomfil  9947  wdomnumr  9950  iunfictbso  10000  dfac2b  10017  dfac9  10023  kmlem13  10049  djuinf  10075  fictb  10130  cfeq0  10142  cff1  10144  cfflb  10145  cofsmo  10155  cfsmolem  10156  coftr  10159  infpssr  10194  fin4en1  10195  fin23lem7  10202  isf34lem4  10263  axcc3  10324  domtriomlem  10328  axdc2lem  10334  axdc3lem2  10337  axdc3lem4  10339  axdc4lem  10341  ac6num  10365  ttukeylem6  10400  ttukeyg  10403  fodomb  10412  iundom2g  10426  alephreg  10468  fpwwe2lem10  10526  fpwwe2lem11  10527  canthp1  10540  pwfseq  10550  gruen  10698  grudomon  10703  gruina  10704  grur1  10706  ltexnq  10861  ltbtwnnq  10864  genpn0  10889  psslinpr  10917  prlem934  10919  ltaddpr  10920  ltexprlem2  10923  ltexprlem6  10927  ltexprlem7  10928  reclem2pr  10934  reclem4pr  10936  suplem1pr  10938  negn0  11541  sup2  12073  supaddc  12084  supmul1  12086  zsupss  12830  fiinfnf1o  14252  hasheqf1oi  14253  hashfun  14339  hashf1  14359  hash3tpexb  14396  rtrclreclem3  14962  rlimdm  15453  climcau  15573  caucvgb  15582  summolem2  15618  zsum  15620  sumz  15624  fsumf1o  15625  fsumss  15627  fsumcl2lem  15633  fsumadd  15642  fsummulc2  15686  fsumconst  15692  fsumrelem  15709  ntrivcvg  15799  prodmolem2  15837  zprod  15839  prod1  15846  fprodf1o  15848  fprodss  15850  fprodcl2lem  15852  fprodmul  15862  fproddiv  15863  fprodconst  15880  fprodn0  15881  ruclem13  16146  4sqlem12  16863  vdwapun  16881  vdwlem9  16896  vdwlem10  16897  ramz  16932  ramub1  16935  firest  17331  mremre  17501  isacs2  17554  iscatd2  17582  cicsym  17706  sscfn1  17719  sscfn2  17720  initoeu2  17918  mgmpropd  18554  gsumval2a  18588  symggen  19377  cyggex2  19804  gsumval3  19814  gsumzres  19816  gsumzcl2  19817  gsumzf1o  19819  gsumzaddlem  19828  gsumconst  19841  gsumzmhm  19844  gsumzoppg  19851  gsum2d2  19881  pgpfac1lem5  19988  ablfaclem3  19996  c0snmgmhm  20375  lss0cl  20875  lspsnat  21077  cnsubrg  21359  gsumfsum  21366  obslbs  21662  lmiclbs  21769  lmisfree  21774  mdetdiaglem  22508  mdet0  22516  eltg3  22872  tgtop  22883  tgidm  22890  ppttop  22917  toponmre  23003  tgrest  23069  neitr  23090  tgcn  23162  cmpsublem  23309  cmpsub  23310  iunconnlem  23337  unconn  23339  1stcfb  23355  2ndcctbss  23365  2ndcdisj  23366  1stcelcls  23371  1stccnp  23372  locfincmp  23436  comppfsc  23442  1stckgen  23464  ptuni2  23486  ptbasfi  23491  ptpjopn  23522  ptclsg  23525  ptcnp  23532  prdstopn  23538  txindis  23544  txtube  23550  txcmplem1  23551  txcmplem2  23552  xkococnlem  23569  txconn  23599  trfbas2  23753  filtop  23765  filconn  23793  filssufilg  23821  fmfnfm  23868  ufldom  23872  hauspwpwf1  23897  alexsubALTlem3  23959  alexsubALT  23961  ptcmplem2  23963  tmdgsum2  24006  tgptsmscld  24061  ustfilxp  24123  xbln0  24324  opnreen  24742  metdsre  24764  cnheibor  24876  phtpc01  24917  cfilfcls  25196  cmetcaulem  25210  iscmet3  25215  ovolctb  25413  ovoliunlem3  25427  ovoliunnul  25430  ovolicc2lem5  25444  ovolicc2  25445  dyadmbl  25523  vitali  25536  itg11  25614  bddmulibl  25762  perfdvf  25826  dvcnp2  25843  dvcnp2OLD  25844  dvlip  25920  dvne0  25938  fta1g  26097  fta1  26238  ulmcau  26326  pserulm  26353  wilthlem2  27001  dchrvmasumif  27436  rpvmasum2  27445  dchrisum0re  27446  dchrisum0lem3  27452  dchrisum0  27453  dchrmusum  27457  dchrvmasum  27458  noinfno  27652  nobdaymin  27711  sltlpss  27848  axcontlem10  28946  usgr1v0e  29299  wlkiswwlks  29849  wlkiswwlkupgr  29851  wlklnwwlkn  29857  wlklnwwlknupgr  29859  umgrwwlks2on  29930  elwwlks2  29939  elwspths2spth  29940  clwlkclwwlklem3  29973  clwlkclwwlkfo  29981  frgr3vlem2  30246  spansncvi  31624  2ndresdju  32623  fnpreimac  32645  gsumwrd2dccatlem  33038  qsidomlem2  33410  reff  33844  locfinreflem  33845  cmpcref  33855  fmcncfil  33936  volmeas  34236  omssubadd  34305  bnj849  34929  r1filimi  35106  acycgrislfgr  35188  derangenlem  35207  cvmsss2  35310  cvmopnlem  35314  cvmfolem  35315  cvmliftmolem2  35318  cvmliftlem15  35334  cvmlift2lem10  35348  cvmlift3lem8  35362  satfdmlem  35404  sat1el2xp  35415  fmlasuc  35422  fundmpss  35803  fnessref  36391  refssfne  36392  neibastop2lem  36394  neibastop2  36395  fnemeet2  36401  fnejoin2  36403  tailfb  36411  knoppcnlem9  36535  isinf2  37439  pibt2  37451  wl-ax13lem1  37528  wl-sbcom2d  37595  matunitlindflem2  37657  poimirlem25  37685  poimirlem27  37687  heicant  37695  itg2addnclem  37711  sdclem1  37783  fdc  37785  istotbnd3  37811  sstotbnd2  37814  prdsbnd2  37835  heibor1lem  37849  heiborlem1  37851  heiborlem10  37860  heibor  37861  riscer  38028  divrngidl  38068  iss2  38372  eqvreldisj  38651  disjlem17  38837  prtlem17  38915  ax12eq  38980  ax12el  38981  ax12inda  38987  ax12v2-o  38988  osumcllem8N  40002  pexmidlem5N  40013  mapdrvallem2  41684  sn-sup2  42524  onexomgt  43274  onexoegt  43277  omabs2  43365  clcnvlem  43656  onfrALT  44582  chordthmALT  44965  relpmin  44985  relpfrlem  44986  modelaxreplem1  45011  wfac8prim  45035  snelmap  45119  ssnnf1octb  45231  choicefi  45237  mapss2  45242  difmap  45244  axccdom  45259  infxrlesupxr  45474  inficc  45574  fsumnncl  45612  stoweidlem43  46081  stoweidlem48  46086  stoweidlem57  46095  stoweidlem60  46098  qndenserrnopn  46336  issalnnd  46383  subsaliuncl  46396  sge0cl  46419  nnfoctbdj  46494  ismeannd  46505  caragenunicl  46562  isomennd  46569  ovn0lem  46603  ovnsubaddlem2  46609  hspdifhsp  46654  hspmbllem3  46666  smflimlem6  46814  smfpimbor1lem1  46836  smfpimcc  46846  smfsuplem2  46850  rlimdmafv  47208  dfatcolem  47286  rlimdmafv2  47289  grimuhgr  47918  grimcnv  47919  grimco  47920  uhgrimedgi  47921  isuspgrim0  47925  gricushgr  47948  gricsym  47952  uhgrimisgrgric  47962  clnbgrgrimlem  47964  clnbgrgrim  47965  grimedg  47966  grtriprop  47972  usgrgrtrirex  47981  isubgr3stgrlem3  47999  uspgrlim  48023  grlimprclnbgredg  48028  grlimgredgex  48031  grlimgrtri  48034  xpco2  48888  opnneilv  48940  thincciso  49485