Theorem exlimdv 1936

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

Syntax hints:   → wi 4  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-ex 1783

This theorem is referenced by:  exlimdvv  1937  exlimddv  1938  ax13lem1  2374  ax13  2375  nfeqf  2381  axc15  2422  sssn  4759  elpreqprb  4798  reusv2lem2  5322  ralxfr2d  5333  euotd  5427  wefrc  5583  wereu2  5586  releldmb  5855  relelrnb  5856  iss  5943  frpomin  6243  onfr  6305  dffv2  6863  dff3  6976  elunirn  7124  fsnex  7155  f1prex  7156  isomin  7208  isofrlem  7211  ovmpt4g  7420  soex  7768  f1oweALT  7815  op1steq  7875  fo2ndf  7962  mpoxopynvov0g  8030  reldmtpos  8050  rntpos  8055  frrlem10  8111  fprresex  8126  wfrlem12OLD  8151  wfrlem17OLD  8156  erdisj  8550  map0g  8672  resixpfo  8724  domdifsn  8841  xpdom3  8857  domunsncan  8859  enfixsn  8868  sucdom2OLD  8869  fodomr  8915  mapdom2  8935  mapdom3  8936  pssnn  8951  ssfiALT  8957  domfi  8975  sucdom2  8989  phplem2  8991  php3  8995  phplem4OLD  9003  php3OLD  9007  pssnnOLD  9040  findcard2OLD  9056  ac6sfi  9058  isfinite2  9072  xpfi  9085  domunfican  9087  fiint  9091  fodomfib  9093  mapfien2  9168  marypha1lem  9192  ordiso  9275  hartogslem1  9301  brwdom2  9332  wdomtr  9334  brwdom3  9341  unwdomg  9343  xpwdomg  9344  unxpwdom2  9347  inf3lem2  9387  ttrclss  9478  dmttrcl  9479  rnttrcl  9480  ttrclselem2  9484  epfrs  9489  tcmin  9499  frmin  9507  cplem1  9647  pm54.43  9759  dfac8alem  9785  dfac8b  9787  dfac8clem  9788  ac10ct  9790  acni2  9802  acndom  9807  numwdom  9815  wdomfil  9817  wdomnumr  9820  iunfictbso  9870  dfac2b  9886  dfac9  9892  kmlem13  9918  djuinf  9944  fictb  10001  cfeq0  10012  cff1  10014  cfflb  10015  cofsmo  10025  cfsmolem  10026  coftr  10029  infpssr  10064  fin4en1  10065  fin23lem7  10072  isf34lem4  10133  axcc3  10194  domtriomlem  10198  axdc2lem  10204  axdc3lem2  10207  axdc3lem4  10209  axdc4lem  10211  ac6num  10235  ttukeylem6  10270  ttukeyg  10273  fodomb  10282  iundom2g  10296  alephreg  10338  fpwwe2lem10  10396  fpwwe2lem11  10397  canthp1  10410  pwfseq  10420  gruen  10568  grudomon  10573  gruina  10574  grur1  10576  ltexnq  10731  ltbtwnnq  10734  genpn0  10759  psslinpr  10787  prlem934  10789  ltaddpr  10790  ltexprlem2  10793  ltexprlem6  10797  ltexprlem7  10798  reclem2pr  10804  reclem4pr  10806  suplem1pr  10808  negn0  11404  sup2  11931  supaddc  11942  supmul1  11944  zsupss  12677  fiinfnf1o  14064  hasheqf1oi  14066  hashfun  14152  hashf1  14171  rtrclreclem3  14771  rlimdm  15260  climcau  15382  caucvgb  15391  summolem2  15428  zsum  15430  sumz  15434  fsumf1o  15435  fsumss  15437  fsumcl2lem  15443  fsumadd  15452  fsummulc2  15496  fsumconst  15502  fsumrelem  15519  ntrivcvg  15609  prodmolem2  15645  zprod  15647  prod1  15654  fprodf1o  15656  fprodss  15658  fprodcl2lem  15660  fprodmul  15670  fproddiv  15671  fprodconst  15688  fprodn0  15689  ruclem13  15951  4sqlem12  16657  vdwapun  16675  vdwlem9  16690  vdwlem10  16691  ramz  16726  ramub1  16729  firest  17143  mremre  17313  isacs2  17362  iscatd2  17390  cicsym  17516  sscfn1  17529  sscfn2  17530  initoeu2  17731  gsumval2a  18369  symggen  19078  cyggex2  19498  gsumval3  19508  gsumzres  19510  gsumzcl2  19511  gsumzf1o  19513  gsumzaddlem  19522  gsumconst  19535  gsumzmhm  19538  gsumzoppg  19545  gsum2d2  19575  pgpfac1lem5  19682  ablfaclem3  19690  lss0cl  20208  lspsnat  20407  cnsubrg  20658  gsumfsum  20665  obslbs  20937  lmiclbs  21044  lmisfree  21049  mdetdiaglem  21747  mdet0  21755  eltg3  22112  tgtop  22123  tgidm  22130  ppttop  22157  toponmre  22244  tgrest  22310  neitr  22331  tgcn  22403  cmpsublem  22550  cmpsub  22551  iunconnlem  22578  unconn  22580  1stcfb  22596  2ndcctbss  22606  2ndcdisj  22607  1stcelcls  22612  1stccnp  22613  locfincmp  22677  comppfsc  22683  1stckgen  22705  ptuni2  22727  ptbasfi  22732  ptpjopn  22763  ptclsg  22766  ptcnp  22773  prdstopn  22779  txindis  22785  txtube  22791  txcmplem1  22792  txcmplem2  22793  xkococnlem  22810  txconn  22840  trfbas2  22994  filtop  23006  filconn  23034  filssufilg  23062  fmfnfm  23109  ufldom  23113  hauspwpwf1  23138  alexsubALTlem3  23200  alexsubALT  23202  ptcmplem2  23204  tmdgsum2  23247  tgptsmscld  23302  ustfilxp  23364  xbln0  23567  opnreen  23994  metdsre  24016  cnheibor  24118  phtpc01  24159  cfilfcls  24438  cmetcaulem  24452  iscmet3  24457  ovolctb  24654  ovoliunlem3  24668  ovoliunnul  24671  ovolicc2lem5  24685  ovolicc2  24686  dyadmbl  24764  vitali  24777  itg11  24855  bddmulibl  25003  perfdvf  25067  dvcnp2  25084  dvlip  25157  dvne0  25175  fta1g  25332  fta1  25468  ulmcau  25554  pserulm  25581  wilthlem2  26218  dchrvmasumif  26651  rpvmasum2  26660  dchrisum0re  26661  dchrisum0lem3  26667  dchrisum0  26668  dchrmusum  26672  dchrvmasum  26673  axcontlem10  27341  usgr1v0e  27693  wlkiswwlks  28241  wlkiswwlkupgr  28243  wlklnwwlkn  28249  wlklnwwlknupgr  28251  umgrwwlks2on  28322  elwwlks2  28331  elwspths2spth  28332  clwlkclwwlklem3  28365  clwlkclwwlkfo  28373  frgr3vlem2  28638  spansncvi  30014  2ndresdju  30986  fnpreimac  31008  qsidomlem2  31629  reff  31789  locfinreflem  31790  cmpcref  31800  fmcncfil  31881  volmeas  32199  omssubadd  32267  bnj849  32905  acycgrislfgr  33114  derangenlem  33133  cvmsss2  33236  cvmopnlem  33240  cvmfolem  33241  cvmliftmolem2  33244  cvmliftlem15  33260  cvmlift2lem10  33274  cvmlift3lem8  33288  satfdmlem  33330  sat1el2xp  33341  fmlasuc  33348  fundmpss  33740  frxp3  33797  noinfno  33921  nocvxmin  33973  sltlpss  34087  fnessref  34546  refssfne  34547  neibastop2lem  34549  neibastop2  34550  fnemeet2  34556  fnejoin2  34558  tailfb  34566  knoppcnlem9  34681  isinf2  35576  pibt2  35588  wl-ax13lem1  35665  wl-sbcom2d  35716  matunitlindflem2  35774  poimirlem25  35802  poimirlem27  35804  heicant  35812  itg2addnclem  35828  sdclem1  35901  fdc  35903  istotbnd3  35929  sstotbnd2  35932  prdsbnd2  35953  heibor1lem  35967  heiborlem1  35969  heiborlem10  35978  heibor  35979  riscer  36146  divrngidl  36186  iss2  36479  eqvreldisj  36727  prtlem17  36890  ax12eq  36955  ax12el  36956  ax12inda  36962  ax12v2-o  36963  osumcllem8N  37977  pexmidlem5N  37988  mapdrvallem2  39659  sn-sup2  40439  clcnvlem  41231  onfrALT  42169  chordthmALT  42553  snelmap  42632  ssnnf1octb  42733  choicefi  42740  mapss2  42745  difmap  42747  axccdom  42762  infxrlesupxr  42976  inficc  43072  fsumnncl  43113  stoweidlem43  43584  stoweidlem48  43589  stoweidlem57  43598  stoweidlem60  43601  qndenserrnopn  43839  issalnnd  43884  subsaliuncl  43897  sge0cl  43919  nnfoctbdj  43994  ismeannd  44005  caragenunicl  44062  isomennd  44069  ovn0lem  44103  ovnsubaddlem2  44109  hspdifhsp  44154  hspmbllem3  44166  smflimlem6  44311  smfpimbor1lem1  44332  smfpimcc  44341  smfsuplem2  44345  rlimdmafv  44669  dfatcolem  44747  rlimdmafv2  44750  isomushgr  45278  isomuspgr  45286  isomgrsym  45288  isomgrtr  45291  mgmpropd  45329  c0snmgmhm  45472  opnneilv  46202  thincciso  46330