Theorem exlimdv 1933

Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2211. (Contributed by NM, 27-Apr-1994.) Remove dependencies on ax-6 1967, ax-7 2007. (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  2378  ax13  2379  nfeqf  2385  axc15  2426  sssn  4802  elpreqprb  4844  reusv2lem2  5369  ralxfr2d  5380  euotd  5488  wefrc  5648  wereu2  5651  releldmb  5926  relelrnb  5927  iss  6022  frpomin  6329  onfr  6391  dffv2  6973  dff3  7089  elunirn  7242  fsnex  7275  f1prex  7276  isomin  7329  isofrlem  7332  ovmpt4g  7552  soex  7915  f1oweALT  7969  op1steq  8030  fo2ndf  8118  frxp3  8148  mpoxopynvov0g  8211  reldmtpos  8231  rntpos  8236  frrlem10  8292  fprresex  8307  wfrlem12OLD  8332  wfrlem17OLD  8337  erdisj  8771  map0g  8896  resixpfo  8948  domdifsn  9066  xpdom3  9082  domunsncan  9084  enfixsn  9093  sucdom2OLD  9094  fodomr  9140  mapdom2  9160  mapdom3  9161  rexdif1en  9170  pssnn  9180  ssfiALT  9186  domfi  9201  sucdom2  9215  phplem2  9217  php3  9221  php3OLD  9231  0sdom1dom  9244  sdom1  9248  1sdom2dom  9253  ac6sfi  9290  isfinite2  9304  xpfiOLD  9329  domunfican  9331  fiint  9336  fiintOLD  9337  fodomfir  9338  fodomfib  9339  fodomfibOLD  9341  mapfien2  9419  marypha1lem  9443  ordiso  9528  hartogslem1  9554  brwdom2  9585  wdomtr  9587  brwdom3  9594  unwdomg  9596  xpwdomg  9597  unxpwdom2  9600  inf3lem2  9641  ttrclss  9732  dmttrcl  9733  rnttrcl  9734  ttrclselem2  9738  epfrs  9743  tcmin  9753  frmin  9761  cplem1  9901  pm54.43  10013  dfac8alem  10041  dfac8b  10043  dfac8clem  10044  ac10ct  10046  acni2  10058  acndom  10063  numwdom  10071  wdomfil  10073  wdomnumr  10076  iunfictbso  10126  dfac2b  10143  dfac9  10149  kmlem13  10175  djuinf  10201  fictb  10256  cfeq0  10268  cff1  10270  cfflb  10271  cofsmo  10281  cfsmolem  10282  coftr  10285  infpssr  10320  fin4en1  10321  fin23lem7  10328  isf34lem4  10389  axcc3  10450  domtriomlem  10454  axdc2lem  10460  axdc3lem2  10463  axdc3lem4  10465  axdc4lem  10467  ac6num  10491  ttukeylem6  10526  ttukeyg  10529  fodomb  10538  iundom2g  10552  alephreg  10594  fpwwe2lem10  10652  fpwwe2lem11  10653  canthp1  10666  pwfseq  10676  gruen  10824  grudomon  10829  gruina  10830  grur1  10832  ltexnq  10987  ltbtwnnq  10990  genpn0  11015  psslinpr  11043  prlem934  11045  ltaddpr  11046  ltexprlem2  11049  ltexprlem6  11053  ltexprlem7  11054  reclem2pr  11060  reclem4pr  11062  suplem1pr  11064  negn0  11664  sup2  12196  supaddc  12207  supmul1  12209  zsupss  12951  fiinfnf1o  14366  hasheqf1oi  14367  hashfun  14453  hashf1  14473  hash3tpexb  14510  rtrclreclem3  15077  rlimdm  15565  climcau  15685  caucvgb  15694  summolem2  15730  zsum  15732  sumz  15736  fsumf1o  15737  fsumss  15739  fsumcl2lem  15745  fsumadd  15754  fsummulc2  15798  fsumconst  15804  fsumrelem  15821  ntrivcvg  15911  prodmolem2  15949  zprod  15951  prod1  15958  fprodf1o  15960  fprodss  15962  fprodcl2lem  15964  fprodmul  15974  fproddiv  15975  fprodconst  15992  fprodn0  15993  ruclem13  16258  4sqlem12  16974  vdwapun  16992  vdwlem9  17007  vdwlem10  17008  ramz  17043  ramub1  17046  firest  17444  mremre  17614  isacs2  17663  iscatd2  17691  cicsym  17815  sscfn1  17828  sscfn2  17829  initoeu2  18027  mgmpropd  18627  gsumval2a  18661  symggen  19449  cyggex2  19876  gsumval3  19886  gsumzres  19888  gsumzcl2  19889  gsumzf1o  19891  gsumzaddlem  19900  gsumconst  19913  gsumzmhm  19916  gsumzoppg  19923  gsum2d2  19953  pgpfac1lem5  20060  ablfaclem3  20068  c0snmgmhm  20420  lss0cl  20902  lspsnat  21104  cnsubrg  21393  gsumfsum  21400  obslbs  21688  lmiclbs  21795  lmisfree  21800  mdetdiaglem  22534  mdet0  22542  eltg3  22898  tgtop  22909  tgidm  22916  ppttop  22943  toponmre  23029  tgrest  23095  neitr  23116  tgcn  23188  cmpsublem  23335  cmpsub  23336  iunconnlem  23363  unconn  23365  1stcfb  23381  2ndcctbss  23391  2ndcdisj  23392  1stcelcls  23397  1stccnp  23398  locfincmp  23462  comppfsc  23468  1stckgen  23490  ptuni2  23512  ptbasfi  23517  ptpjopn  23548  ptclsg  23551  ptcnp  23558  prdstopn  23564  txindis  23570  txtube  23576  txcmplem1  23577  txcmplem2  23578  xkococnlem  23595  txconn  23625  trfbas2  23779  filtop  23791  filconn  23819  filssufilg  23847  fmfnfm  23894  ufldom  23898  hauspwpwf1  23923  alexsubALTlem3  23985  alexsubALT  23987  ptcmplem2  23989  tmdgsum2  24032  tgptsmscld  24087  ustfilxp  24149  xbln0  24351  opnreen  24769  metdsre  24791  cnheibor  24903  phtpc01  24944  cfilfcls  25224  cmetcaulem  25238  iscmet3  25243  ovolctb  25441  ovoliunlem3  25455  ovoliunnul  25458  ovolicc2lem5  25472  ovolicc2  25473  dyadmbl  25551  vitali  25564  itg11  25642  bddmulibl  25790  perfdvf  25854  dvcnp2  25871  dvcnp2OLD  25872  dvlip  25948  dvne0  25966  fta1g  26125  fta1  26266  ulmcau  26354  pserulm  26381  wilthlem2  27029  dchrvmasumif  27464  rpvmasum2  27473  dchrisum0re  27474  dchrisum0lem3  27480  dchrisum0  27481  dchrmusum  27485  dchrvmasum  27486  noinfno  27680  nocvxmin  27740  sltlpss  27862  axcontlem10  28898  usgr1v0e  29251  wlkiswwlks  29804  wlkiswwlkupgr  29806  wlklnwwlkn  29812  wlklnwwlknupgr  29814  umgrwwlks2on  29885  elwwlks2  29894  elwspths2spth  29895  clwlkclwwlklem3  29928  clwlkclwwlkfo  29936  frgr3vlem2  30201  spansncvi  31579  2ndresdju  32573  fnpreimac  32595  gsumwrd2dccatlem  33006  qsidomlem2  33414  reff  33816  locfinreflem  33817  cmpcref  33827  fmcncfil  33908  volmeas  34208  omssubadd  34278  bnj849  34902  acycgrislfgr  35120  derangenlem  35139  cvmsss2  35242  cvmopnlem  35246  cvmfolem  35247  cvmliftmolem2  35250  cvmliftlem15  35266  cvmlift2lem10  35280  cvmlift3lem8  35294  satfdmlem  35336  sat1el2xp  35347  fmlasuc  35354  fundmpss  35730  fnessref  36321  refssfne  36322  neibastop2lem  36324  neibastop2  36325  fnemeet2  36331  fnejoin2  36333  tailfb  36341  knoppcnlem9  36465  isinf2  37369  pibt2  37381  wl-ax13lem1  37458  wl-sbcom2d  37525  matunitlindflem2  37587  poimirlem25  37615  poimirlem27  37617  heicant  37625  itg2addnclem  37641  sdclem1  37713  fdc  37715  istotbnd3  37741  sstotbnd2  37744  prdsbnd2  37765  heibor1lem  37779  heiborlem1  37781  heiborlem10  37790  heibor  37791  riscer  37958  divrngidl  37998  iss2  38308  eqvreldisj  38578  disjlem17  38763  prtlem17  38840  ax12eq  38905  ax12el  38906  ax12inda  38912  ax12v2-o  38913  osumcllem8N  39928  pexmidlem5N  39939  mapdrvallem2  41610  sn-sup2  42461  onexomgt  43212  onexoegt  43215  omabs2  43303  clcnvlem  43594  onfrALT  44522  chordthmALT  44905  relpmin  44925  relpfrlem  44926  modelaxreplem1  44951  wfac8prim  44975  snelmap  45054  ssnnf1octb  45166  choicefi  45172  mapss2  45177  difmap  45179  axccdom  45194  infxrlesupxr  45411  inficc  45511  fsumnncl  45549  stoweidlem43  46020  stoweidlem48  46025  stoweidlem57  46034  stoweidlem60  46037  qndenserrnopn  46275  issalnnd  46322  subsaliuncl  46335  sge0cl  46358  nnfoctbdj  46433  ismeannd  46444  caragenunicl  46501  isomennd  46508  ovn0lem  46542  ovnsubaddlem2  46548  hspdifhsp  46593  hspmbllem3  46605  smflimlem6  46753  smfpimbor1lem1  46775  smfpimcc  46785  smfsuplem2  46789  rlimdmafv  47154  dfatcolem  47232  rlimdmafv2  47235  grimuhgr  47848  grimcnv  47849  grimco  47850  uhgrimedgi  47851  isuspgrim0  47855  gricushgr  47878  gricsym  47882  uhgrimisgrgric  47892  clnbgrgrimlem  47894  clnbgrgrim  47895  grimedg  47896  grtriprop  47901  usgrgrtrirex  47910  isubgr3stgrlem3  47928  uspgrlim  47952  grlimgrtri  47956  opnneilv  48831  thincciso  49287