Theorem exlimdv 1932

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

Syntax hints:   → wi 4  ∃wex 1778

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909

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

This theorem is referenced by:  exlimdvv  1933  exlimddv  1934  ax13lem1  2377  ax13  2378  nfeqf  2384  axc15  2425  sssn  4806  elpreqprb  4848  reusv2lem2  5379  ralxfr2d  5390  euotd  5498  wefrc  5659  wereu2  5662  releldmb  5937  relelrnb  5938  iss  6033  frpomin  6340  onfr  6402  dffv2  6984  dff3  7100  elunirn  7253  fsnex  7285  f1prex  7286  isomin  7339  isofrlem  7342  ovmpt4g  7562  soex  7925  f1oweALT  7979  op1steq  8040  fo2ndf  8128  frxp3  8158  mpoxopynvov0g  8221  reldmtpos  8241  rntpos  8246  frrlem10  8302  fprresex  8317  wfrlem12OLD  8342  wfrlem17OLD  8347  erdisj  8781  map0g  8906  resixpfo  8958  domdifsn  9076  xpdom3  9092  domunsncan  9094  enfixsn  9103  sucdom2OLD  9104  fodomr  9150  mapdom2  9170  mapdom3  9171  rexdif1en  9180  pssnn  9190  ssfiALT  9196  domfi  9211  sucdom2  9225  phplem2  9227  php3  9231  phplem4OLD  9239  php3OLD  9243  0sdom1dom  9256  sdom1  9260  1sdom2dom  9265  ac6sfi  9302  isfinite2  9316  xpfiOLD  9341  domunfican  9343  fiint  9348  fiintOLD  9349  fodomfir  9350  fodomfib  9351  fodomfibOLD  9353  mapfien2  9431  marypha1lem  9455  ordiso  9538  hartogslem1  9564  brwdom2  9595  wdomtr  9597  brwdom3  9604  unwdomg  9606  xpwdomg  9607  unxpwdom2  9610  inf3lem2  9651  ttrclss  9742  dmttrcl  9743  rnttrcl  9744  ttrclselem2  9748  epfrs  9753  tcmin  9763  frmin  9771  cplem1  9911  pm54.43  10023  dfac8alem  10051  dfac8b  10053  dfac8clem  10054  ac10ct  10056  acni2  10068  acndom  10073  numwdom  10081  wdomfil  10083  wdomnumr  10086  iunfictbso  10136  dfac2b  10153  dfac9  10159  kmlem13  10185  djuinf  10211  fictb  10266  cfeq0  10278  cff1  10280  cfflb  10281  cofsmo  10291  cfsmolem  10292  coftr  10295  infpssr  10330  fin4en1  10331  fin23lem7  10338  isf34lem4  10399  axcc3  10460  domtriomlem  10464  axdc2lem  10470  axdc3lem2  10473  axdc3lem4  10475  axdc4lem  10477  ac6num  10501  ttukeylem6  10536  ttukeyg  10539  fodomb  10548  iundom2g  10562  alephreg  10604  fpwwe2lem10  10662  fpwwe2lem11  10663  canthp1  10676  pwfseq  10686  gruen  10834  grudomon  10839  gruina  10840  grur1  10842  ltexnq  10997  ltbtwnnq  11000  genpn0  11025  psslinpr  11053  prlem934  11055  ltaddpr  11056  ltexprlem2  11059  ltexprlem6  11063  ltexprlem7  11064  reclem2pr  11070  reclem4pr  11072  suplem1pr  11074  negn0  11674  sup2  12206  supaddc  12217  supmul1  12219  zsupss  12961  fiinfnf1o  14372  hasheqf1oi  14373  hashfun  14459  hashf1  14479  hash3tpexb  14516  rtrclreclem3  15082  rlimdm  15570  climcau  15690  caucvgb  15699  summolem2  15735  zsum  15737  sumz  15741  fsumf1o  15742  fsumss  15744  fsumcl2lem  15750  fsumadd  15759  fsummulc2  15803  fsumconst  15809  fsumrelem  15826  ntrivcvg  15916  prodmolem2  15954  zprod  15956  prod1  15963  fprodf1o  15965  fprodss  15967  fprodcl2lem  15969  fprodmul  15979  fproddiv  15980  fprodconst  15997  fprodn0  15998  ruclem13  16261  4sqlem12  16977  vdwapun  16995  vdwlem9  17010  vdwlem10  17011  ramz  17046  ramub1  17049  firest  17449  mremre  17619  isacs2  17668  iscatd2  17696  cicsym  17820  sscfn1  17833  sscfn2  17834  initoeu2  18033  mgmpropd  18634  gsumval2a  18668  symggen  19457  cyggex2  19884  gsumval3  19894  gsumzres  19896  gsumzcl2  19897  gsumzf1o  19899  gsumzaddlem  19908  gsumconst  19921  gsumzmhm  19924  gsumzoppg  19931  gsum2d2  19961  pgpfac1lem5  20068  ablfaclem3  20076  c0snmgmhm  20431  lss0cl  20914  lspsnat  21116  cnsubrg  21408  gsumfsum  21415  obslbs  21705  lmiclbs  21812  lmisfree  21817  mdetdiaglem  22553  mdet0  22561  eltg3  22917  tgtop  22928  tgidm  22935  ppttop  22962  toponmre  23048  tgrest  23114  neitr  23135  tgcn  23207  cmpsublem  23354  cmpsub  23355  iunconnlem  23382  unconn  23384  1stcfb  23400  2ndcctbss  23410  2ndcdisj  23411  1stcelcls  23416  1stccnp  23417  locfincmp  23481  comppfsc  23487  1stckgen  23509  ptuni2  23531  ptbasfi  23536  ptpjopn  23567  ptclsg  23570  ptcnp  23577  prdstopn  23583  txindis  23589  txtube  23595  txcmplem1  23596  txcmplem2  23597  xkococnlem  23614  txconn  23644  trfbas2  23798  filtop  23810  filconn  23838  filssufilg  23866  fmfnfm  23913  ufldom  23917  hauspwpwf1  23942  alexsubALTlem3  24004  alexsubALT  24006  ptcmplem2  24008  tmdgsum2  24051  tgptsmscld  24106  ustfilxp  24168  xbln0  24370  opnreen  24790  metdsre  24812  cnheibor  24924  phtpc01  24965  cfilfcls  25245  cmetcaulem  25259  iscmet3  25264  ovolctb  25462  ovoliunlem3  25476  ovoliunnul  25479  ovolicc2lem5  25493  ovolicc2  25494  dyadmbl  25572  vitali  25585  itg11  25663  bddmulibl  25811  perfdvf  25875  dvcnp2  25892  dvcnp2OLD  25893  dvlip  25969  dvne0  25987  fta1g  26146  fta1  26287  ulmcau  26375  pserulm  26402  wilthlem2  27049  dchrvmasumif  27484  rpvmasum2  27493  dchrisum0re  27494  dchrisum0lem3  27500  dchrisum0  27501  dchrmusum  27505  dchrvmasum  27506  noinfno  27700  nocvxmin  27760  sltlpss  27882  axcontlem10  28919  usgr1v0e  29272  wlkiswwlks  29825  wlkiswwlkupgr  29827  wlklnwwlkn  29833  wlklnwwlknupgr  29835  umgrwwlks2on  29906  elwwlks2  29915  elwspths2spth  29916  clwlkclwwlklem3  29949  clwlkclwwlkfo  29957  frgr3vlem2  30222  spansncvi  31600  2ndresdju  32595  fnpreimac  32617  gsumwrd2dccatlem  33013  qsidomlem2  33421  reff  33813  locfinreflem  33814  cmpcref  33824  fmcncfil  33905  volmeas  34207  omssubadd  34277  bnj849  34914  acycgrislfgr  35132  derangenlem  35151  cvmsss2  35254  cvmopnlem  35258  cvmfolem  35259  cvmliftmolem2  35262  cvmliftlem15  35278  cvmlift2lem10  35292  cvmlift3lem8  35306  satfdmlem  35348  sat1el2xp  35359  fmlasuc  35366  fundmpss  35742  fnessref  36333  refssfne  36334  neibastop2lem  36336  neibastop2  36337  fnemeet2  36343  fnejoin2  36345  tailfb  36353  knoppcnlem9  36477  isinf2  37381  pibt2  37393  wl-ax13lem1  37470  wl-sbcom2d  37537  matunitlindflem2  37599  poimirlem25  37627  poimirlem27  37629  heicant  37637  itg2addnclem  37653  sdclem1  37725  fdc  37727  istotbnd3  37753  sstotbnd2  37756  prdsbnd2  37777  heibor1lem  37791  heiborlem1  37793  heiborlem10  37802  heibor  37803  riscer  37970  divrngidl  38010  iss2  38320  eqvreldisj  38590  disjlem17  38775  prtlem17  38852  ax12eq  38917  ax12el  38918  ax12inda  38924  ax12v2-o  38925  osumcllem8N  39940  pexmidlem5N  39951  mapdrvallem2  41622  sn-sup2  42480  onexomgt  43231  onexoegt  43234  omabs2  43322  clcnvlem  43613  onfrALT  44541  chordthmALT  44925  relpmin  44945  relpfrlem  44946  modelaxreplem1  44967  wfac8prim  44991  snelmap  45059  ssnnf1octb  45171  choicefi  45177  mapss2  45182  difmap  45184  axccdom  45199  infxrlesupxr  45419  inficc  45519  fsumnncl  45559  stoweidlem43  46030  stoweidlem48  46035  stoweidlem57  46044  stoweidlem60  46047  qndenserrnopn  46285  issalnnd  46332  subsaliuncl  46345  sge0cl  46368  nnfoctbdj  46443  ismeannd  46454  caragenunicl  46511  isomennd  46518  ovn0lem  46552  ovnsubaddlem2  46558  hspdifhsp  46603  hspmbllem3  46615  smflimlem6  46763  smfpimbor1lem1  46785  smfpimcc  46795  smfsuplem2  46799  rlimdmafv  47162  dfatcolem  47240  rlimdmafv2  47243  isuspgrim0  47845  grimuhgr  47851  grimcnv  47852  grimco  47853  gricushgr  47859  gricsym  47863  uhgrimisgrgric  47872  clnbgrgrimlem  47874  clnbgrgrim  47875  grimedg  47876  grtriprop  47881  usgrgrtrirex  47890  isubgr3stgrlem3  47908  uspgrlim  47932  grlimgrtri  47936  opnneilv  48790  thincciso  49154