Theorem exlimdv 1933

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

Syntax hints:   → wi 4  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  exlimdvv  1934  exlimddv  1935  ax13lem1  2372  ax13  2373  nfeqf  2379  axc15  2420  sssn  4786  elpreqprb  4828  reusv2lem2  5349  ralxfr2d  5360  euotd  5468  wefrc  5625  wereu2  5628  releldmb  5899  relelrnb  5900  iss  5995  frpomin  6301  onfr  6359  dffv2  6938  dff3  7054  elunirn  7207  fsnex  7240  f1prex  7241  isomin  7294  isofrlem  7297  ovmpt4g  7516  soex  7877  f1oweALT  7930  op1steq  7991  fo2ndf  8077  frxp3  8107  mpoxopynvov0g  8170  reldmtpos  8190  rntpos  8195  frrlem10  8251  fprresex  8266  erdisj  8705  map0g  8834  resixpfo  8886  domdifsn  9001  xpdom3  9016  domunsncan  9018  enfixsn  9027  fodomr  9069  mapdom2  9089  mapdom3  9090  rexdif1en  9099  pssnn  9109  ssfiALT  9115  domfi  9130  sucdom2  9144  phplem2  9146  php3  9150  0sdom1dom  9162  sdom1  9166  1sdom2dom  9170  ac6sfi  9207  isfinite2  9221  xpfiOLD  9246  domunfican  9248  fiint  9253  fiintOLD  9254  fodomfir  9255  fodomfib  9256  fodomfibOLD  9258  mapfien2  9336  marypha1lem  9360  ordiso  9445  hartogslem1  9471  brwdom2  9502  wdomtr  9504  brwdom3  9511  unwdomg  9513  xpwdomg  9514  unxpwdom2  9517  inf3lem2  9558  ttrclss  9649  dmttrcl  9650  rnttrcl  9651  ttrclselem2  9655  epfrs  9660  tcmin  9670  frmin  9678  cplem1  9818  pm54.43  9930  dfac8alem  9958  dfac8b  9960  dfac8clem  9961  ac10ct  9963  acni2  9975  acndom  9980  numwdom  9988  wdomfil  9990  wdomnumr  9993  iunfictbso  10043  dfac2b  10060  dfac9  10066  kmlem13  10092  djuinf  10118  fictb  10173  cfeq0  10185  cff1  10187  cfflb  10188  cofsmo  10198  cfsmolem  10199  coftr  10202  infpssr  10237  fin4en1  10238  fin23lem7  10245  isf34lem4  10306  axcc3  10367  domtriomlem  10371  axdc2lem  10377  axdc3lem2  10380  axdc3lem4  10382  axdc4lem  10384  ac6num  10408  ttukeylem6  10443  ttukeyg  10446  fodomb  10455  iundom2g  10469  alephreg  10511  fpwwe2lem10  10569  fpwwe2lem11  10570  canthp1  10583  pwfseq  10593  gruen  10741  grudomon  10746  gruina  10747  grur1  10749  ltexnq  10904  ltbtwnnq  10907  genpn0  10932  psslinpr  10960  prlem934  10962  ltaddpr  10963  ltexprlem2  10966  ltexprlem6  10970  ltexprlem7  10971  reclem2pr  10977  reclem4pr  10979  suplem1pr  10981  negn0  11583  sup2  12115  supaddc  12126  supmul1  12128  zsupss  12872  fiinfnf1o  14291  hasheqf1oi  14292  hashfun  14378  hashf1  14398  hash3tpexb  14435  rtrclreclem3  15002  rlimdm  15493  climcau  15613  caucvgb  15622  summolem2  15658  zsum  15660  sumz  15664  fsumf1o  15665  fsumss  15667  fsumcl2lem  15673  fsumadd  15682  fsummulc2  15726  fsumconst  15732  fsumrelem  15749  ntrivcvg  15839  prodmolem2  15877  zprod  15879  prod1  15886  fprodf1o  15888  fprodss  15890  fprodcl2lem  15892  fprodmul  15902  fproddiv  15903  fprodconst  15920  fprodn0  15921  ruclem13  16186  4sqlem12  16903  vdwapun  16921  vdwlem9  16936  vdwlem10  16937  ramz  16972  ramub1  16975  firest  17371  mremre  17541  isacs2  17590  iscatd2  17618  cicsym  17742  sscfn1  17755  sscfn2  17756  initoeu2  17954  mgmpropd  18554  gsumval2a  18588  symggen  19376  cyggex2  19803  gsumval3  19813  gsumzres  19815  gsumzcl2  19816  gsumzf1o  19818  gsumzaddlem  19827  gsumconst  19840  gsumzmhm  19843  gsumzoppg  19850  gsum2d2  19880  pgpfac1lem5  19987  ablfaclem3  19995  c0snmgmhm  20347  lss0cl  20829  lspsnat  21031  cnsubrg  21320  gsumfsum  21327  obslbs  21615  lmiclbs  21722  lmisfree  21727  mdetdiaglem  22461  mdet0  22469  eltg3  22825  tgtop  22836  tgidm  22843  ppttop  22870  toponmre  22956  tgrest  23022  neitr  23043  tgcn  23115  cmpsublem  23262  cmpsub  23263  iunconnlem  23290  unconn  23292  1stcfb  23308  2ndcctbss  23318  2ndcdisj  23319  1stcelcls  23324  1stccnp  23325  locfincmp  23389  comppfsc  23395  1stckgen  23417  ptuni2  23439  ptbasfi  23444  ptpjopn  23475  ptclsg  23478  ptcnp  23485  prdstopn  23491  txindis  23497  txtube  23503  txcmplem1  23504  txcmplem2  23505  xkococnlem  23522  txconn  23552  trfbas2  23706  filtop  23718  filconn  23746  filssufilg  23774  fmfnfm  23821  ufldom  23825  hauspwpwf1  23850  alexsubALTlem3  23912  alexsubALT  23914  ptcmplem2  23916  tmdgsum2  23959  tgptsmscld  24014  ustfilxp  24076  xbln0  24278  opnreen  24696  metdsre  24718  cnheibor  24830  phtpc01  24871  cfilfcls  25150  cmetcaulem  25164  iscmet3  25169  ovolctb  25367  ovoliunlem3  25381  ovoliunnul  25384  ovolicc2lem5  25398  ovolicc2  25399  dyadmbl  25477  vitali  25490  itg11  25568  bddmulibl  25716  perfdvf  25780  dvcnp2  25797  dvcnp2OLD  25798  dvlip  25874  dvne0  25892  fta1g  26051  fta1  26192  ulmcau  26280  pserulm  26307  wilthlem2  26955  dchrvmasumif  27390  rpvmasum2  27399  dchrisum0re  27400  dchrisum0lem3  27406  dchrisum0  27407  dchrmusum  27411  dchrvmasum  27412  noinfno  27606  nocvxmin  27666  sltlpss  27795  axcontlem10  28876  usgr1v0e  29229  wlkiswwlks  29779  wlkiswwlkupgr  29781  wlklnwwlkn  29787  wlklnwwlknupgr  29789  umgrwwlks2on  29860  elwwlks2  29869  elwspths2spth  29870  clwlkclwwlklem3  29903  clwlkclwwlkfo  29911  frgr3vlem2  30176  spansncvi  31554  2ndresdju  32546  fnpreimac  32568  gsumwrd2dccatlem  32979  qsidomlem2  33397  reff  33802  locfinreflem  33803  cmpcref  33813  fmcncfil  33894  volmeas  34194  omssubadd  34264  bnj849  34888  acycgrislfgr  35112  derangenlem  35131  cvmsss2  35234  cvmopnlem  35238  cvmfolem  35239  cvmliftmolem2  35242  cvmliftlem15  35258  cvmlift2lem10  35272  cvmlift3lem8  35286  satfdmlem  35328  sat1el2xp  35339  fmlasuc  35346  fundmpss  35727  fnessref  36318  refssfne  36319  neibastop2lem  36321  neibastop2  36322  fnemeet2  36328  fnejoin2  36330  tailfb  36338  knoppcnlem9  36462  isinf2  37366  pibt2  37378  wl-ax13lem1  37455  wl-sbcom2d  37522  matunitlindflem2  37584  poimirlem25  37612  poimirlem27  37614  heicant  37622  itg2addnclem  37638  sdclem1  37710  fdc  37712  istotbnd3  37738  sstotbnd2  37741  prdsbnd2  37762  heibor1lem  37776  heiborlem1  37778  heiborlem10  37787  heibor  37788  riscer  37955  divrngidl  37995  iss2  38299  eqvreldisj  38578  disjlem17  38764  prtlem17  38842  ax12eq  38907  ax12el  38908  ax12inda  38914  ax12v2-o  38915  osumcllem8N  39930  pexmidlem5N  39941  mapdrvallem2  41612  sn-sup2  42452  onexomgt  43203  onexoegt  43206  omabs2  43294  clcnvlem  43585  onfrALT  44512  chordthmALT  44895  relpmin  44915  relpfrlem  44916  modelaxreplem1  44941  wfac8prim  44965  snelmap  45049  ssnnf1octb  45161  choicefi  45167  mapss2  45172  difmap  45174  axccdom  45189  infxrlesupxr  45405  inficc  45505  fsumnncl  45543  stoweidlem43  46014  stoweidlem48  46019  stoweidlem57  46028  stoweidlem60  46031  qndenserrnopn  46269  issalnnd  46316  subsaliuncl  46329  sge0cl  46352  nnfoctbdj  46427  ismeannd  46438  caragenunicl  46495  isomennd  46502  ovn0lem  46536  ovnsubaddlem2  46542  hspdifhsp  46587  hspmbllem3  46599  smflimlem6  46747  smfpimbor1lem1  46769  smfpimcc  46779  smfsuplem2  46783  rlimdmafv  47151  dfatcolem  47229  rlimdmafv2  47232  grimuhgr  47860  grimcnv  47861  grimco  47862  uhgrimedgi  47863  isuspgrim0  47867  gricushgr  47890  gricsym  47894  uhgrimisgrgric  47904  clnbgrgrimlem  47906  clnbgrgrim  47907  grimedg  47908  grtriprop  47913  usgrgrtrirex  47922  isubgr3stgrlem3  47940  uspgrlim  47964  grlimgrtri  47968  xpco2  48818  opnneilv  48870  thincciso  49415