Theorem exlimdv 1934

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 1970, ax-7 2015. (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 209  df-ex 1781

This theorem is referenced by:  exlimdvv  1935  exlimddv  1936  ax13lem1  2392  ax13  2393  nfeqf  2399  axc15  2444  sssn  4759  elpreqprb  4798  reusv2lem2  5300  ralxfr2d  5311  euotd  5403  wefrc  5549  wereu2  5552  releldmb  5816  relelrnb  5817  iss  5903  onfr  6230  dffv2  6756  dff3  6866  elunirn  7010  fsnex  7039  f1prex  7040  isomin  7090  isofrlem  7093  ovmpt4g  7297  soex  7626  f1oweALT  7673  op1steq  7733  fo2ndf  7817  mpoxopynvov0g  7880  reldmtpos  7900  rntpos  7905  wfrlem12  7966  wfrlem17  7971  erdisj  8341  map0g  8448  resixpfo  8500  domdifsn  8600  xpdom3  8615  domunsncan  8617  enfixsn  8626  fodomr  8668  mapdom2  8688  mapdom3  8689  phplem4  8699  php3  8703  sucdom2  8714  pssnn  8736  ssfi  8738  domfi  8739  findcard2  8758  ac6sfi  8762  isfinite2  8776  xpfi  8789  domunfican  8791  fiint  8795  fodomfib  8798  mapfien2  8872  marypha1lem  8897  ordiso  8980  hartogslem1  9006  brwdom2  9037  wdomtr  9039  brwdom3  9046  unwdomg  9048  xpwdomg  9049  unxpwdom2  9052  inf3lem2  9092  epfrs  9173  tcmin  9183  cplem1  9318  pm54.43  9429  dfac8alem  9455  dfac8b  9457  dfac8clem  9458  ac10ct  9460  acni2  9472  acndom  9477  numwdom  9485  wdomfil  9487  wdomnumr  9490  iunfictbso  9540  dfac2b  9556  dfac9  9562  kmlem13  9588  djuinf  9614  fictb  9667  cfeq0  9678  cff1  9680  cfflb  9681  cofsmo  9691  cfsmolem  9692  coftr  9695  infpssr  9730  fin4en1  9731  fin23lem7  9738  isf34lem4  9799  axcc3  9860  domtriomlem  9864  axdc2lem  9870  axdc3lem2  9873  axdc3lem4  9875  axdc4lem  9877  ac6num  9901  ttukeylem6  9936  ttukeyg  9939  fodomb  9948  iundom2g  9962  alephreg  10004  fpwwe2lem11  10062  fpwwe2lem12  10063  canthp1  10076  pwfseq  10086  gruen  10234  grudomon  10239  gruina  10240  grur1  10242  ltexnq  10397  ltbtwnnq  10400  genpn0  10425  psslinpr  10453  prlem934  10455  ltaddpr  10456  ltexprlem2  10459  ltexprlem6  10463  ltexprlem7  10464  reclem2pr  10470  reclem4pr  10472  suplem1pr  10474  negn0  11069  sup2  11597  supaddc  11608  supmul1  11610  zsupss  12338  fiinfnf1o  13711  hasheqf1oi  13713  hashfun  13799  hashf1  13816  rtrclreclem3  14419  rlimdm  14908  climcau  15027  caucvgb  15036  summolem2  15073  zsum  15075  sumz  15079  fsumf1o  15080  fsumss  15082  fsumcl2lem  15088  fsumadd  15096  fsummulc2  15139  fsumconst  15145  fsumrelem  15162  ntrivcvg  15253  prodmolem2  15289  zprod  15291  prod1  15298  fprodf1o  15300  fprodss  15302  fprodcl2lem  15304  fprodmul  15314  fproddiv  15315  fprodconst  15332  fprodn0  15333  ruclem13  15595  4sqlem12  16292  vdwapun  16310  vdwlem9  16325  vdwlem10  16326  ramz  16361  ramub1  16364  firest  16706  mremre  16875  isacs2  16924  iscatd2  16952  cicsym  17074  sscfn1  17087  sscfn2  17088  initoeu2  17276  gsumval2a  17895  symggen  18598  cyggex2  19017  gsumval3  19027  gsumzres  19029  gsumzcl2  19030  gsumzf1o  19032  gsumzaddlem  19041  gsumconst  19054  gsumzmhm  19057  gsumzoppg  19064  gsum2d2  19094  pgpfac1lem5  19201  ablfaclem3  19209  lss0cl  19718  lspsnat  19917  cnsubrg  20605  gsumfsum  20612  obslbs  20874  lmiclbs  20981  lmisfree  20986  mdetdiaglem  21207  mdet0  21215  eltg3  21570  tgtop  21581  tgidm  21588  ppttop  21615  toponmre  21701  tgrest  21767  neitr  21788  tgcn  21860  cmpsublem  22007  cmpsub  22008  iunconnlem  22035  unconn  22037  1stcfb  22053  2ndcctbss  22063  2ndcdisj  22064  1stcelcls  22069  1stccnp  22070  locfincmp  22134  comppfsc  22140  1stckgen  22162  ptuni2  22184  ptbasfi  22189  ptpjopn  22220  ptclsg  22223  ptcnp  22230  prdstopn  22236  txindis  22242  txtube  22248  txcmplem1  22249  txcmplem2  22250  xkococnlem  22267  txconn  22297  trfbas2  22451  filtop  22463  filconn  22491  filssufilg  22519  fmfnfm  22566  ufldom  22570  hauspwpwf1  22595  alexsubALTlem3  22657  alexsubALT  22659  ptcmplem2  22661  tmdgsum2  22704  tgptsmscld  22759  ustfilxp  22821  xbln0  23024  opnreen  23439  metdsre  23461  cnheibor  23559  phtpc01  23600  cfilfcls  23877  cmetcaulem  23891  iscmet3  23896  ovolctb  24091  ovoliunlem3  24105  ovoliunnul  24108  ovolicc2lem5  24122  ovolicc2  24123  dyadmbl  24201  vitali  24214  itg11  24292  bddmulibl  24439  perfdvf  24501  dvcnp2  24517  dvlip  24590  dvne0  24608  fta1g  24761  fta1  24897  ulmcau  24983  pserulm  25010  wilthlem2  25646  dchrvmasumif  26079  rpvmasum2  26088  dchrisum0re  26089  dchrisum0lem3  26095  dchrisum0  26096  dchrmusum  26100  dchrvmasum  26101  axcontlem10  26759  usgr1v0e  27108  wlkiswwlks  27654  wlkiswwlkupgr  27656  wlklnwwlkn  27662  wlklnwwlknupgr  27664  umgrwwlks2on  27736  elwwlks2  27745  elwspths2spth  27746  clwlkclwwlklem3  27779  clwlkclwwlkfo  27787  frgr3vlem2  28053  spansncvi  29429  fnpreimac  30416  qsidomlem2  30966  reff  31103  locfinreflem  31104  cmpcref  31114  fmcncfil  31174  volmeas  31490  omssubadd  31558  bnj849  32197  acycgrislfgr  32399  derangenlem  32418  cvmsss2  32521  cvmopnlem  32525  cvmfolem  32526  cvmliftmolem2  32529  cvmliftlem15  32545  cvmlift2lem10  32559  cvmlift3lem8  32573  satfdmlem  32615  sat1el2xp  32626  fmlasuc  32633  fundmpss  33009  frpomin  33078  frmin  33084  frrlem10  33132  nocvxmin  33248  fnessref  33705  refssfne  33706  neibastop2lem  33708  neibastop2  33709  fnemeet2  33715  fnejoin2  33717  tailfb  33725  knoppcnlem9  33840  isinf2  34689  pibt2  34701  wl-ax13lem1  34761  wl-sbcom2d  34812  matunitlindflem2  34904  poimirlem25  34932  poimirlem27  34934  heicant  34942  itg2addnclem  34958  sdclem1  35033  fdc  35035  istotbnd3  35064  sstotbnd2  35067  prdsbnd2  35088  heibor1lem  35102  heiborlem1  35104  heiborlem10  35113  heibor  35114  riscer  35281  divrngidl  35321  iss2  35616  eqvreldisj  35864  prtlem17  36027  ax12eq  36092  ax12el  36093  ax12inda  36099  ax12v2-o  36100  osumcllem8N  37114  pexmidlem5N  37125  mapdrvallem2  38796  clcnvlem  40032  onfrALT  40932  chordthmALT  41316  snelmap  41395  ssnnf1octb  41505  choicefi  41512  mapss2  41517  difmap  41519  axccdom  41536  infxrlesupxr  41759  inficc  41859  fsumnncl  41901  stoweidlem43  42377  stoweidlem48  42382  stoweidlem57  42391  stoweidlem60  42394  qndenserrnopn  42632  issalnnd  42677  subsaliuncl  42690  sge0cl  42712  nnfoctbdj  42787  ismeannd  42798  caragenunicl  42855  isomennd  42862  ovn0lem  42896  ovnsubaddlem2  42902  hspdifhsp  42947  hspmbllem3  42959  smflimlem6  43101  smfpimbor1lem1  43122  smfpimcc  43131  smfsuplem2  43135  rlimdmafv  43425  dfatcolem  43503  rlimdmafv2  43506  isomushgr  44040  isomuspgr  44048  isomgrsym  44050  isomgrtr  44053  mgmpropd  44091  c0snmgmhm  44234