Theorem exlimdv 1915

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

Syntax hints:   → wi 4  ∃wex 1765

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892

This theorem depends on definitions:  df-bi 208  df-ex 1766

This theorem is referenced by:  exlimdvv  1916  exlimddv  1917  sbcom2OLD  2250  ax13lem1  2348  ax13  2349  nfeqf  2356  axc15  2402  axc15OLD  2403  sssn  4672  elpreqprb  4711  reusv2lem2  5198  ralxfr2d  5209  euotd  5301  wefrc  5444  wereu2  5447  releldmb  5705  relelrnb  5706  iss  5791  onfr  6112  dffv2  6630  dff3  6736  elunirn  6882  fsnex  6911  f1prex  6912  isomin  6960  isofrlem  6963  ovmpt4g  7160  soex  7489  f1oweALT  7536  op1steq  7596  fo2ndf  7677  mpoxopynvov0g  7738  reldmtpos  7758  rntpos  7763  wfrlem12  7825  wfrlem17  7830  erdisj  8198  map0g  8305  resixpfo  8355  domdifsn  8454  xpdom3  8469  domunsncan  8471  enfixsn  8480  fodomr  8522  mapdom2  8542  mapdom3  8543  phplem4  8553  php3  8557  sucdom2  8567  pssnn  8589  ssfi  8591  domfi  8592  findcard2  8611  ac6sfi  8615  isfinite2  8629  xpfi  8642  domunfican  8644  fiint  8648  fodomfib  8651  mapfien2  8725  marypha1lem  8750  ordiso  8833  hartogslem1  8859  brwdom2  8890  wdomtr  8892  brwdom3  8899  unwdomg  8901  xpwdomg  8902  unxpwdom2  8905  inf3lem2  8945  epfrs  9026  tcmin  9036  cplem1  9171  pm54.43  9282  dfac8alem  9308  dfac8b  9310  dfac8clem  9311  ac10ct  9313  acni2  9325  acndom  9330  numwdom  9338  wdomfil  9340  wdomnumr  9343  iunfictbso  9393  dfac2b  9409  dfac9  9415  kmlem13  9441  djuinf  9467  fictb  9520  cfeq0  9531  cff1  9533  cfflb  9534  cofsmo  9544  cfsmolem  9545  coftr  9548  infpssr  9583  fin4en1  9584  fin23lem7  9591  isf34lem4  9652  axcc3  9713  domtriomlem  9717  axdc2lem  9723  axdc3lem2  9726  axdc3lem4  9728  axdc4lem  9730  ac6num  9754  ttukeylem6  9789  ttukeyg  9792  fodomb  9801  iundom2g  9815  alephreg  9857  fpwwe2lem11  9915  fpwwe2lem12  9916  canthp1  9929  pwfseq  9939  gruen  10087  grudomon  10092  gruina  10093  grur1  10095  ltexnq  10250  ltbtwnnq  10253  genpn0  10278  psslinpr  10306  prlem934  10308  ltaddpr  10309  ltexprlem2  10312  ltexprlem6  10316  ltexprlem7  10317  reclem2pr  10323  reclem4pr  10325  suplem1pr  10327  negn0  10923  sup2  11451  supaddc  11462  supmul1  11464  zsupss  12190  fiinfnf1o  13564  hasheqf1oi  13566  hashfun  13650  hashf1  13667  rtrclreclem3  14257  rlimdm  14746  climcau  14865  caucvgb  14874  summolem2  14910  zsum  14912  sumz  14916  fsumf1o  14917  fsumss  14919  fsumcl2lem  14925  fsumadd  14933  fsummulc2  14976  fsumconst  14982  fsumrelem  14999  ntrivcvg  15090  prodmolem2  15126  zprod  15128  prod1  15135  fprodf1o  15137  fprodss  15139  fprodcl2lem  15141  fprodmul  15151  fproddiv  15152  fprodconst  15169  fprodn0  15170  ruclem13  15432  4sqlem12  16125  vdwapun  16143  vdwlem9  16158  vdwlem10  16159  ramz  16194  ramub1  16197  firest  16539  mremre  16708  isacs2  16757  iscatd2  16785  cicsym  16907  sscfn1  16920  sscfn2  16921  initoeu2  17109  gsumval2a  17722  symggen  18333  cyggex2  18742  gsumval3  18752  gsumzres  18754  gsumzcl2  18755  gsumzf1o  18757  gsumzaddlem  18765  gsumconst  18778  gsumzmhm  18781  gsumzoppg  18788  gsum2d2  18818  pgpfac1lem5  18922  ablfaclem3  18930  lss0cl  19412  lspsnat  19611  cnsubrg  20291  gsumfsum  20298  obslbs  20560  lmiclbs  20667  lmisfree  20672  mdetdiaglem  20895  mdet0  20903  eltg3  21258  tgtop  21269  tgidm  21276  ppttop  21303  toponmre  21389  tgrest  21455  neitr  21476  tgcn  21548  cmpsublem  21695  cmpsub  21696  iunconnlem  21723  unconn  21725  1stcfb  21741  2ndcctbss  21751  2ndcdisj  21752  1stcelcls  21757  1stccnp  21758  locfincmp  21822  comppfsc  21828  1stckgen  21850  ptuni2  21872  ptbasfi  21877  ptpjopn  21908  ptclsg  21911  ptcnp  21918  prdstopn  21924  txindis  21930  txtube  21936  txcmplem1  21937  txcmplem2  21938  xkococnlem  21955  txconn  21985  trfbas2  22139  filtop  22151  filconn  22179  filssufilg  22207  fmfnfm  22254  ufldom  22258  hauspwpwf1  22283  alexsubALTlem3  22345  alexsubALT  22347  ptcmplem2  22349  tmdgsum2  22392  tgptsmscld  22446  ustfilxp  22508  xbln0  22711  opnreen  23126  metdsre  23148  cnheibor  23246  phtpc01  23287  cfilfcls  23564  cmetcaulem  23578  iscmet3  23583  ovolctb  23778  ovoliunlem3  23792  ovoliunnul  23795  ovolicc2lem5  23809  ovolicc2  23810  dyadmbl  23888  vitali  23901  itg11  23979  bddmulibl  24126  perfdvf  24188  dvcnp2  24204  dvlip  24277  dvne0  24295  fta1g  24448  fta1  24584  ulmcau  24670  pserulm  24697  wilthlem2  25332  dchrvmasumif  25765  rpvmasum2  25774  dchrisum0re  25775  dchrisum0lem3  25781  dchrisum0  25782  dchrmusum  25786  dchrvmasum  25787  axcontlem10  26446  usgr1v0e  26795  wlkiswwlks  27340  wlkiswwlkupgr  27342  wlklnwwlkn  27348  wlklnwwlknupgr  27350  umgrwwlks2on  27422  elwwlks2  27431  elwspths2spth  27432  clwlkclwwlklem3  27465  clwlkclwwlkfo  27473  frgr3vlem2  27741  spansncvi  29116  fnpreimac  30102  reff  30716  locfinreflem  30717  cmpcref  30727  fmcncfil  30787  volmeas  31103  omssubadd  31171  bnj849  31809  acycgrislfgr  32009  derangenlem  32028  cvmsss2  32131  cvmopnlem  32135  cvmfolem  32136  cvmliftmolem2  32139  cvmliftlem15  32155  cvmlift2lem10  32169  cvmlift3lem8  32183  satfdmlem  32225  sat1el2xp  32236  fmlasuc  32243  fundmpss  32619  frpomin  32689  frmin  32695  frrlem10  32743  nocvxmin  32859  fnessref  33316  refssfne  33317  neibastop2lem  33319  neibastop2  33320  fnemeet2  33326  fnejoin2  33328  tailfb  33336  knoppcnlem9  33451  isinf2  34238  pibt2  34250  wl-ax13lem1  34298  wl-sbcom2d  34349  matunitlindflem2  34441  poimirlem25  34469  poimirlem27  34471  heicant  34479  itg2addnclem  34495  sdclem1  34571  fdc  34573  istotbnd3  34602  sstotbnd2  34605  prdsbnd2  34626  heibor1lem  34640  heiborlem1  34642  heiborlem10  34651  heibor  34652  riscer  34819  divrngidl  34859  iss2  35154  eqvreldisj  35401  prtlem17  35564  ax12eq  35629  ax12el  35630  ax12inda  35636  ax12v2-o  35637  osumcllem8N  36651  pexmidlem5N  36662  mapdrvallem2  38333  clcnvlem  39489  onfrALT  40443  chordthmALT  40827  snelmap  40906  ssnnf1octb  41017  choicefi  41024  mapss2  41029  difmap  41031  axccdom  41048  infxrlesupxr  41273  inficc  41373  fsumnncl  41415  stoweidlem43  41892  stoweidlem48  41897  stoweidlem57  41906  stoweidlem60  41909  qndenserrnopn  42147  issalnnd  42192  subsaliuncl  42205  sge0cl  42227  nnfoctbdj  42302  ismeannd  42313  caragenunicl  42370  isomennd  42377  ovn0lem  42411  ovnsubaddlem2  42417  hspdifhsp  42462  hspmbllem3  42474  smflimlem6  42616  smfpimbor1lem1  42637  smfpimcc  42646  smfsuplem2  42650  rlimdmafv  42914  dfatcolem  42992  rlimdmafv2  42995  isomushgr  43495  isomuspgr  43503  isomgrsym  43505  isomgrtr  43508  mgmpropd  43546  c0snmgmhm  43685