Theorem exlimdv 1929

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

Syntax hints:   → wi 4  ∃wex 1774

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906

This theorem depends on definitions:  df-bi 206  df-ex 1775

This theorem is referenced by:  exlimdvv  1930  exlimddv  1931  ax13lem1  2368  ax13  2369  nfeqf  2375  axc15  2416  sssn  4825  elpreqprb  4864  reusv2lem2  5393  ralxfr2d  5404  euotd  5509  wefrc  5666  wereu2  5669  releldmb  5942  relelrnb  5943  iss  6033  frpomin  6340  onfr  6402  dffv2  6987  dff3  7104  elunirn  7255  fsnex  7286  f1prex  7287  isomin  7339  isofrlem  7342  ovmpt4g  7562  soex  7923  f1oweALT  7970  op1steq  8031  fo2ndf  8120  frxp3  8150  mpoxopynvov0g  8213  reldmtpos  8233  rntpos  8238  frrlem10  8294  fprresex  8309  wfrlem12OLD  8334  wfrlem17OLD  8339  erdisj  8771  map0g  8896  resixpfo  8948  domdifsn  9072  xpdom3  9088  domunsncan  9090  enfixsn  9099  sucdom2OLD  9100  fodomr  9146  mapdom2  9166  mapdom3  9167  rexdif1en  9176  pssnn  9186  ssfiALT  9192  domfi  9210  sucdom2  9224  phplem2  9226  php3  9230  phplem4OLD  9238  php3OLD  9242  0sdom1dom  9256  sdom1  9260  1sdom2dom  9265  pssnnOLD  9283  findcard2OLD  9302  ac6sfi  9305  isfinite2  9319  xpfiOLD  9336  domunfican  9338  fiint  9342  fodomfib  9344  mapfien2  9426  marypha1lem  9450  ordiso  9533  hartogslem1  9559  brwdom2  9590  wdomtr  9592  brwdom3  9599  unwdomg  9601  xpwdomg  9602  unxpwdom2  9605  inf3lem2  9646  ttrclss  9737  dmttrcl  9738  rnttrcl  9739  ttrclselem2  9743  epfrs  9748  tcmin  9758  frmin  9766  cplem1  9906  pm54.43  10018  dfac8alem  10046  dfac8b  10048  dfac8clem  10049  ac10ct  10051  acni2  10063  acndom  10068  numwdom  10076  wdomfil  10078  wdomnumr  10081  iunfictbso  10131  dfac2b  10147  dfac9  10153  kmlem13  10179  djuinf  10205  fictb  10262  cfeq0  10273  cff1  10275  cfflb  10276  cofsmo  10286  cfsmolem  10287  coftr  10290  infpssr  10325  fin4en1  10326  fin23lem7  10333  isf34lem4  10394  axcc3  10455  domtriomlem  10459  axdc2lem  10465  axdc3lem2  10468  axdc3lem4  10470  axdc4lem  10472  ac6num  10496  ttukeylem6  10531  ttukeyg  10534  fodomb  10543  iundom2g  10557  alephreg  10599  fpwwe2lem10  10657  fpwwe2lem11  10658  canthp1  10671  pwfseq  10681  gruen  10829  grudomon  10834  gruina  10835  grur1  10837  ltexnq  10992  ltbtwnnq  10995  genpn0  11020  psslinpr  11048  prlem934  11050  ltaddpr  11051  ltexprlem2  11054  ltexprlem6  11058  ltexprlem7  11059  reclem2pr  11065  reclem4pr  11067  suplem1pr  11069  negn0  11667  sup2  12194  supaddc  12205  supmul1  12207  zsupss  12945  fiinfnf1o  14335  hasheqf1oi  14336  hashfun  14422  hashf1  14444  rtrclreclem3  15033  rlimdm  15521  climcau  15643  caucvgb  15652  summolem2  15688  zsum  15690  sumz  15694  fsumf1o  15695  fsumss  15697  fsumcl2lem  15703  fsumadd  15712  fsummulc2  15756  fsumconst  15762  fsumrelem  15779  ntrivcvg  15869  prodmolem2  15905  zprod  15907  prod1  15914  fprodf1o  15916  fprodss  15918  fprodcl2lem  15920  fprodmul  15930  fproddiv  15931  fprodconst  15948  fprodn0  15949  ruclem13  16212  4sqlem12  16918  vdwapun  16936  vdwlem9  16951  vdwlem10  16952  ramz  16987  ramub1  16990  firest  17407  mremre  17577  isacs2  17626  iscatd2  17654  cicsym  17780  sscfn1  17793  sscfn2  17794  initoeu2  17998  mgmpropd  18604  gsumval2a  18638  symggen  19418  cyggex2  19845  gsumval3  19855  gsumzres  19857  gsumzcl2  19858  gsumzf1o  19860  gsumzaddlem  19869  gsumconst  19882  gsumzmhm  19885  gsumzoppg  19892  gsum2d2  19922  pgpfac1lem5  20029  ablfaclem3  20037  c0snmgmhm  20394  lss0cl  20824  lspsnat  21026  cnsubrg  21353  gsumfsum  21360  obslbs  21657  lmiclbs  21764  lmisfree  21769  mdetdiaglem  22493  mdet0  22501  eltg3  22858  tgtop  22869  tgidm  22876  ppttop  22903  toponmre  22990  tgrest  23056  neitr  23077  tgcn  23149  cmpsublem  23296  cmpsub  23297  iunconnlem  23324  unconn  23326  1stcfb  23342  2ndcctbss  23352  2ndcdisj  23353  1stcelcls  23358  1stccnp  23359  locfincmp  23423  comppfsc  23429  1stckgen  23451  ptuni2  23473  ptbasfi  23478  ptpjopn  23509  ptclsg  23512  ptcnp  23519  prdstopn  23525  txindis  23531  txtube  23537  txcmplem1  23538  txcmplem2  23539  xkococnlem  23556  txconn  23586  trfbas2  23740  filtop  23752  filconn  23780  filssufilg  23808  fmfnfm  23855  ufldom  23859  hauspwpwf1  23884  alexsubALTlem3  23946  alexsubALT  23948  ptcmplem2  23950  tmdgsum2  23993  tgptsmscld  24048  ustfilxp  24110  xbln0  24313  opnreen  24740  metdsre  24762  cnheibor  24874  phtpc01  24915  cfilfcls  25195  cmetcaulem  25209  iscmet3  25214  ovolctb  25412  ovoliunlem3  25426  ovoliunnul  25429  ovolicc2lem5  25443  ovolicc2  25444  dyadmbl  25522  vitali  25535  itg11  25613  bddmulibl  25761  perfdvf  25825  dvcnp2  25842  dvcnp2OLD  25843  dvlip  25919  dvne0  25937  fta1g  26097  fta1  26236  ulmcau  26324  pserulm  26351  wilthlem2  26994  dchrvmasumif  27429  rpvmasum2  27438  dchrisum0re  27439  dchrisum0lem3  27445  dchrisum0  27446  dchrmusum  27450  dchrvmasum  27451  noinfno  27644  nocvxmin  27704  sltlpss  27826  axcontlem10  28777  usgr1v0e  29132  wlkiswwlks  29680  wlkiswwlkupgr  29682  wlklnwwlkn  29688  wlklnwwlknupgr  29690  umgrwwlks2on  29761  elwwlks2  29770  elwspths2spth  29771  clwlkclwwlklem3  29804  clwlkclwwlkfo  29812  frgr3vlem2  30077  spansncvi  31455  2ndresdju  32428  fnpreimac  32450  qsidomlem2  33159  reff  33430  locfinreflem  33431  cmpcref  33441  fmcncfil  33522  volmeas  33840  omssubadd  33910  bnj849  34546  acycgrislfgr  34752  derangenlem  34771  cvmsss2  34874  cvmopnlem  34878  cvmfolem  34879  cvmliftmolem2  34882  cvmliftlem15  34898  cvmlift2lem10  34912  cvmlift3lem8  34926  satfdmlem  34968  sat1el2xp  34979  fmlasuc  34986  fundmpss  35352  fnessref  35831  refssfne  35832  neibastop2lem  35834  neibastop2  35835  fnemeet2  35841  fnejoin2  35843  tailfb  35851  knoppcnlem9  35966  isinf2  36874  pibt2  36886  wl-ax13lem1  36963  wl-sbcom2d  37017  matunitlindflem2  37079  poimirlem25  37107  poimirlem27  37109  heicant  37117  itg2addnclem  37133  sdclem1  37205  fdc  37207  istotbnd3  37233  sstotbnd2  37236  prdsbnd2  37257  heibor1lem  37271  heiborlem1  37273  heiborlem10  37282  heibor  37283  riscer  37450  divrngidl  37490  iss2  37805  eqvreldisj  38075  disjlem17  38260  prtlem17  38337  ax12eq  38402  ax12el  38403  ax12inda  38409  ax12v2-o  38410  osumcllem8N  39425  pexmidlem5N  39436  mapdrvallem2  41107  sn-sup2  41996  onexomgt  42641  onexoegt  42644  omabs2  42733  clcnvlem  43025  onfrALT  43960  chordthmALT  44344  snelmap  44420  ssnnf1octb  44539  choicefi  44545  mapss2  44550  difmap  44552  axccdom  44567  infxrlesupxr  44790  inficc  44891  fsumnncl  44932  stoweidlem43  45403  stoweidlem48  45408  stoweidlem57  45417  stoweidlem60  45420  qndenserrnopn  45658  issalnnd  45705  subsaliuncl  45718  sge0cl  45741  nnfoctbdj  45816  ismeannd  45827  caragenunicl  45884  isomennd  45891  ovn0lem  45925  ovnsubaddlem2  45931  hspdifhsp  45976  hspmbllem3  45988  smflimlem6  46136  smfpimbor1lem1  46158  smfpimcc  46168  smfsuplem2  46172  rlimdmafv  46529  dfatcolem  46607  rlimdmafv2  46610  isuspgrim0  47142  grimuhgr  47148  grimcnv  47149  grimco  47150  gricushgr  47155  gricsym  47159  opnneilv  47899  thincciso  48027