Theorem exlimdv 1935

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

Syntax hints:   → wi 4  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

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

This theorem is referenced by:  exlimdvv  1936  exlimddv  1937  ax13lem1  2378  ax13  2379  nfeqf  2385  axc15  2426  sssn  4769  elpreqprb  4811  reusv2lem2  5341  ralxfr2d  5352  euotd  5467  wefrc  5625  wereu2  5628  releldmb  5901  relelrnb  5902  iss  6000  frpomin  6304  onfr  6362  dffv2  6935  dff3  7052  elunirn  7206  fsnex  7238  f1prex  7239  isomin  7292  isofrlem  7295  ovmpt4g  7514  soex  7872  f1oweALT  7925  op1steq  7986  fo2ndf  8071  frxp3  8101  mpoxopynvov0g  8164  reldmtpos  8184  rntpos  8189  frrlem10  8245  fprresex  8260  erdisj  8701  map0g  8832  resixpfo  8884  domdifsn  8998  xpdom3  9013  domunsncan  9015  enfixsn  9024  fodomr  9066  mapdom2  9086  mapdom3  9087  rexdif1en  9095  pssnn  9103  ssfiALT  9108  domfi  9123  sucdom2  9137  phplem2  9139  php3  9143  0sdom1dom  9156  sdom1  9160  1sdom2dom  9164  ac6sfi  9194  isfinite2  9208  domunfican  9232  fiint  9237  fodomfir  9238  fodomfib  9239  fodomfibOLD  9241  mapfien2  9322  marypha1lem  9346  ordiso  9431  hartogslem1  9457  brwdom2  9488  wdomtr  9490  brwdom3  9497  unwdomg  9499  xpwdomg  9500  unxpwdom2  9503  inf3lem2  9550  ttrclss  9641  dmttrcl  9642  rnttrcl  9643  ttrclselem2  9647  epfrs  9652  tcmin  9660  frmin  9673  cplem1  9813  pm54.43  9925  dfac8alem  9951  dfac8b  9953  dfac8clem  9954  ac10ct  9956  acni2  9968  acndom  9973  numwdom  9981  wdomfil  9983  wdomnumr  9986  iunfictbso  10036  dfac2b  10053  dfac9  10059  kmlem13  10085  djuinf  10111  fictb  10166  cfeq0  10178  cff1  10180  cfflb  10181  cofsmo  10191  cfsmolem  10192  coftr  10195  infpssr  10230  fin4en1  10231  fin23lem7  10238  isf34lem4  10299  axcc3  10360  domtriomlem  10364  axdc2lem  10370  axdc3lem2  10373  axdc3lem4  10375  axdc4lem  10377  ac6num  10401  ttukeylem6  10436  ttukeyg  10439  fodomb  10448  iundom2g  10462  alephreg  10505  fpwwe2lem10  10563  fpwwe2lem11  10564  canthp1  10577  pwfseq  10587  gruen  10735  grudomon  10740  gruina  10741  grur1  10743  ltexnq  10898  ltbtwnnq  10901  genpn0  10926  psslinpr  10954  prlem934  10956  ltaddpr  10957  ltexprlem2  10960  ltexprlem6  10964  ltexprlem7  10965  reclem2pr  10971  reclem4pr  10973  suplem1pr  10975  negn0  11579  sup2  12112  supaddc  12123  supmul1  12125  zsupss  12887  fiinfnf1o  14312  hasheqf1oi  14313  hashfun  14399  hashf1  14419  hash3tpexb  14456  rtrclreclem3  15022  rlimdm  15513  climcau  15633  caucvgb  15642  summolem2  15678  zsum  15680  sumz  15684  fsumf1o  15685  fsumss  15687  fsumcl2lem  15693  fsumadd  15702  fsummulc2  15746  fsumconst  15752  fsumrelem  15770  ntrivcvg  15862  prodmolem2  15900  zprod  15902  prod1  15909  fprodf1o  15911  fprodss  15913  fprodcl2lem  15915  fprodmul  15925  fproddiv  15926  fprodconst  15943  fprodn0  15944  ruclem13  16209  4sqlem12  16927  vdwapun  16945  vdwlem9  16960  vdwlem10  16961  ramz  16996  ramub1  16999  firest  17395  mremre  17566  isacs2  17619  iscatd2  17647  cicsym  17771  sscfn1  17784  sscfn2  17785  initoeu2  17983  mgmpropd  18619  gsumval2a  18653  symggen  19445  cyggex2  19872  gsumval3  19882  gsumzres  19884  gsumzcl2  19885  gsumzf1o  19887  gsumzaddlem  19896  gsumconst  19909  gsumzmhm  19912  gsumzoppg  19919  gsum2d2  19949  pgpfac1lem5  20056  ablfaclem3  20064  c0snmgmhm  20442  lss0cl  20942  lspsnat  21143  cnsubrg  21407  gsumfsum  21414  obslbs  21710  lmiclbs  21817  lmisfree  21822  mdetdiaglem  22563  mdet0  22571  eltg3  22927  tgtop  22938  tgidm  22945  ppttop  22972  toponmre  23058  tgrest  23124  neitr  23145  tgcn  23217  cmpsublem  23364  cmpsub  23365  iunconnlem  23392  unconn  23394  1stcfb  23410  2ndcctbss  23420  2ndcdisj  23421  1stcelcls  23426  1stccnp  23427  locfincmp  23491  comppfsc  23497  1stckgen  23519  ptuni2  23541  ptbasfi  23546  ptpjopn  23577  ptclsg  23580  ptcnp  23587  prdstopn  23593  txindis  23599  txtube  23605  txcmplem1  23606  txcmplem2  23607  xkococnlem  23624  txconn  23654  trfbas2  23808  filtop  23820  filconn  23848  filssufilg  23876  fmfnfm  23923  ufldom  23927  hauspwpwf1  23952  alexsubALTlem3  24014  alexsubALT  24016  ptcmplem2  24018  tmdgsum2  24061  tgptsmscld  24116  ustfilxp  24178  xbln0  24379  opnreen  24797  metdsre  24819  cnheibor  24922  phtpc01  24963  cfilfcls  25241  cmetcaulem  25255  iscmet3  25260  ovolctb  25457  ovoliunlem3  25471  ovoliunnul  25474  ovolicc2lem5  25488  ovolicc2  25489  dyadmbl  25567  vitali  25580  itg11  25658  bddmulibl  25806  perfdvf  25870  dvcnp2  25887  dvlip  25960  dvne0  25978  fta1g  26135  fta1  26274  ulmcau  26360  pserulm  26387  wilthlem2  27032  dchrvmasumif  27466  rpvmasum2  27475  dchrisum0re  27476  dchrisum0lem3  27482  dchrisum0  27483  dchrmusum  27487  dchrvmasum  27488  noinfno  27682  nobdaymin  27745  ltslpss  27900  axcontlem10  29042  usgr1v0e  29395  wlkiswwlks  29944  wlkiswwlkupgr  29946  wlklnwwlkn  29952  wlklnwwlknupgr  29954  usgrwwlks2on  30026  umgrwwlks2on  30027  elwwlks2  30037  elwspths2spth  30038  clwlkclwwlklem3  30071  clwlkclwwlkfo  30079  frgr3vlem2  30344  spansncvi  31723  2ndresdju  32722  fnpreimac  32743  gsumwrd2dccatlem  33138  qsidomlem2  33513  reff  33983  locfinreflem  33984  cmpcref  33994  fmcncfil  34075  volmeas  34375  omssubadd  34444  bnj849  35067  r1filimi  35246  acycgrislfgr  35334  derangenlem  35353  cvmsss2  35456  cvmopnlem  35460  cvmfolem  35461  cvmliftmolem2  35464  cvmliftlem15  35480  cvmlift2lem10  35494  cvmlift3lem8  35508  satfdmlem  35550  sat1el2xp  35561  fmlasuc  35568  fundmpss  35949  fnessref  36539  refssfne  36540  neibastop2lem  36542  neibastop2  36543  fnemeet2  36549  fnejoin2  36551  tailfb  36559  axuntco  36661  dfttc4lem2  36711  knoppcnlem9  36761  isinf2  37721  pibt2  37733  wl-ax13lem1  37810  wl-sbcom2d  37886  matunitlindflem2  37938  poimirlem25  37966  poimirlem27  37968  heicant  37976  itg2addnclem  37992  sdclem1  38064  fdc  38066  istotbnd3  38092  sstotbnd2  38095  prdsbnd2  38116  heibor1lem  38130  heiborlem1  38132  heiborlem10  38141  heibor  38142  riscer  38309  divrngidl  38349  iss2  38665  eqvreldisj  39019  disjlem17  39223  prtlem17  39322  ax12eq  39387  ax12el  39388  ax12inda  39394  ax12v2-o  39395  osumcllem8N  40409  pexmidlem5N  40420  mapdrvallem2  42091  sn-sup2  42936  onexomgt  43669  onexoegt  43672  omabs2  43760  clcnvlem  44050  onfrALT  44976  chordthmALT  45359  relpmin  45379  relpfrlem  45380  modelaxreplem1  45405  wfac8prim  45429  snelmap  45513  ssnnf1octb  45624  choicefi  45629  mapss2  45634  difmap  45636  axccdom  45651  infxrlesupxr  45864  inficc  45964  fsumnncl  46002  stoweidlem43  46471  stoweidlem48  46476  stoweidlem57  46485  stoweidlem60  46488  qndenserrnopn  46726  issalnnd  46773  subsaliuncl  46786  sge0cl  46809  nnfoctbdj  46884  ismeannd  46895  caragenunicl  46952  isomennd  46959  ovn0lem  46993  ovnsubaddlem2  46999  hspdifhsp  47044  hspmbllem3  47056  smflimlem6  47204  smfpimbor1lem1  47226  smfpimcc  47236  smfsuplem2  47240  rlimdmafv  47625  dfatcolem  47703  rlimdmafv2  47706  grimuhgr  48363  grimcnv  48364  grimco  48365  uhgrimedgi  48366  isuspgrim0  48370  gricushgr  48393  gricsym  48397  uhgrimisgrgric  48407  clnbgrgrimlem  48409  clnbgrgrim  48410  grimedg  48411  grtriprop  48417  usgrgrtrirex  48426  isubgr3stgrlem3  48444  uspgrlim  48468  grlimprclnbgredg  48473  grlimgredgex  48476  grlimgrtri  48479  xpco2  49332  opnneilv  49384  thincciso  49928