Theorem exlimdv 1966

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  exlimdvv  1967  exlimddv  1968  ax13lem1  2403  ax13  2404  nfeqf  2410  axc15  2451  sssn  4787  elpreqprb  4828  reusv2lem2  5364  ralxfr2d  5375  euotd  5490  wefrc  5649  wereu2  5652  releldmb  5930  relelrnb  5931  iss  6031  frpomin  6338  onfr  6397  dffv2  6973  dff3  7093  elunirn  7248  fsnex  7284  f1prex  7285  isomin  7338  isofrlem  7341  ovmpt4g  7560  soex  7918  f1oweALT  7969  op1steq  8030  fo2ndf  8118  frxp3  8149  mpoxopynvov0g  8212  reldmtpos  8232  rntpos  8237  frrlem10  8294  fprresex  8309  erdisj  8754  map0g  8891  resixpfo  8943  domdifsn  9058  xpdom3  9073  domunsncan  9075  enfixsn  9084  fodomr  9126  mapdom2  9146  mapdom3  9147  rexdif1en  9155  pssnn  9163  ssfiALT  9168  domfi  9183  sucdom2  9197  phplem2  9199  php3  9203  0sdom1dom  9216  sdom1  9220  1sdom2dom  9224  ac6sfi  9254  isfinite2  9268  domunfican  9291  fiint  9296  fodomfir  9297  fodomfib  9298  mapfien2  9379  marypha1lem  9403  ordiso  9488  hartogslem1  9514  brwdom2  9545  wdomtr  9547  brwdom3  9554  unwdomg  9556  xpwdomg  9557  unxpwdom2  9560  inf3lem2  9608  ttrclss  9699  dmttrcl  9700  rnttrcl  9701  ttrclselem2  9705  epfrs  9710  tcmin  9718  frmin  9731  cplem1  9889  cplem1OLD  9890  karden  9898  pm54.43  10006  dfac8alem  10032  dfac8b  10034  dfac8clem  10035  ac10ct  10037  acni2  10049  acndom  10054  numwdom  10062  wdomfil  10064  wdomnumr  10067  iunfictbso  10117  dfac2b  10133  dfac9  10139  kmlem13  10165  djuinf  10191  fictb  10246  cfeq0  10258  cff1  10260  cfflb  10261  cofsmo  10271  cfsmolem  10272  coftr  10275  infpssr  10310  fin4en1  10311  fin23lem7  10318  isf34lem4  10379  axcc3  10440  domtriomlem  10444  axdc2lem  10450  axdc3lem2  10453  axdc3lem4  10455  axdc4lem  10457  ac6num  10481  ttukeylem6  10516  ttukeyg  10519  fodomb  10529  iundom2g  10548  alephreg  10591  fpwwe2lem10  10649  fpwwe2lem11  10650  canthp1  10663  pwfseq  10673  gruen  10821  grudomon  10826  gruina  10827  grur1  10829  ltexnq  10984  ltbtwnnq  10987  genpn0  11012  psslinpr  11040  prlem934  11042  ltaddpr  11043  ltexprlem2  11046  ltexprlem6  11050  ltexprlem7  11051  reclem2pr  11057  reclem4pr  11059  suplem1pr  11061  negn0  11667  sup2  12195  supaddc  12206  supmul1  12208  zsupss  12986  fiinfnf1o  14414  hasheqf1oi  14415  hashfun  14502  hashf1  14522  hash3tpexb  14559  rtrclreclem3  15133  rlimdm  15638  climcau  15758  caucvgb  15767  summolem2  15802  zsum  15804  sumz  15808  fsumf1o  15809  fsumss  15811  fsumcl2lem  15817  fsumadd  15826  fsummulc2  15870  fsumconst  15876  fsumrelem  15894  ntrivcvg  15986  prodmolem2  16022  zprod  16024  prod1  16031  fprodf1o  16033  fprodss  16035  fprodcl2lem  16037  fprodmul  16047  fproddiv  16048  fprodconst  16065  fprodn0  16066  ruclem13  16330  4sqlem12  17048  vdwapun  17066  vdwlem9  17081  vdwlem10  17082  ramz  17117  ramub1  17120  firest  17517  mremre  17688  isacs2  17741  iscatd2  17769  cicsym  17893  sscfn1  17906  sscfn2  17907  initoeu2  18105  mgmpropd  18743  gsumval2a  18787  symggen  19597  cyggex2  20024  gsumval3  20034  gsumzres  20036  gsumzcl2  20037  gsumzf1o  20039  gsumzaddlem  20048  gsumconst  20061  gsumzmhm  20064  gsumzoppg  20071  gsum2d2  20101  pgpfac1lem5  20208  ablfaclem3  20216  c0snmgmhm  20603  lss0cl  21131  lspsnat  21332  qsidomlem2  21544  cnsubrg  21640  gsumfsum  21647  obslbs  21943  lmiclbs  22050  lmisfree  22055  mdetdiaglem  22820  mdet0  22828  matunitlindflem2  22902  eltg3  23187  tgtop  23198  tgidm  23205  ppttop  23232  toponmre  23318  tgrest  23384  neitr  23405  tgcn  23477  cmpsublem  23624  cmpsub  23625  iunconnlem  23652  unconn  23654  1stcfb  23670  2ndcctbss  23681  2ndcdisj  23682  1stcelcls  23687  1stccnp  23688  locfincmp  23752  comppfsc  23758  1stckgen  23780  ptuni2  23802  ptbasfi  23807  ptpjopn  23838  ptclsg  23841  ptcnp  23848  prdstopn  23854  txindis  23860  txtube  23866  txcmplem1  23867  txcmplem2  23868  xkococnlem  23885  txconn  23915  trfbas2  24069  filtop  24081  filconn  24109  filssufilg  24137  fmfnfm  24184  ufldom  24188  hauspwpwf1  24213  alexsubALTlem3  24275  alexsubALT  24277  ptcmplem2  24279  tmdgsum2  24322  tgptsmscld  24377  ustfilxp  24439  xbln0  24640  opnreen  25058  metdsre  25080  cnheibor  25183  phtpc01  25224  cfilfcls  25502  cmetcaulem  25516  iscmet3  25521  ovolctb  25718  ovoliunlem3  25732  ovoliunnul  25735  ovolicc2lem5  25749  ovolicc2  25750  dyadmbl  25828  vitali  25841  itg11  25919  bddmulibl  26066  perfdvf  26130  dvcnp2  26147  dvlip  26220  dvne0  26238  fta1g  26395  fta1  26538  ulmcau  26631  pserulm  26658  wilthlem2  27305  dchrvmasumif  27739  rpvmasum2  27748  dchrisum0re  27749  dchrisum0lem3  27755  dchrisum0  27756  dchrmusum  27760  dchrvmasum  27761  noinfno  27954  nobdaymin  28018  ltslpss  28173  axcontlem10  29430  usgr1v0e  29786  wlkiswwlks  30344  wlkiswwlkupgr  30346  wlklnwwlkn  30352  wlklnwwlknupgr  30354  usgrwwlks2on  30426  umgrwwlks2on  30427  elwwlks2  30437  elwspths2spth  30438  clwlkclwwlklem3  30471  clwlkclwwlkfo  30479  frgr3vlem2  30754  spansncvi  32133  2ndresdju  33122  fnpreimac  33143  gsumwrd2dccatlem  33517  reff  34349  locfinreflem  34350  cmpcref  34360  fmcncfil  34441  volmeas  34742  omssubadd  34811  bnj849  35434  r1filimi  35611  kardfi  35696  onvfowev  35713  acycgrislfgr  35731  derangenlem  35750  cvmsss2  35853  cvmopnlem  35857  cvmfolem  35858  cvmliftmolem2  35861  cvmliftlem15  35877  cvmlift2lem10  35891  cvmlift3lem8  35905  satfdmlem  35947  sat1el2xp  35958  fmlasuc  35965  fundmpss  36346  fnessref  36976  refssfne  36977  neibastop2lem  36979  neibastop2  36980  fnemeet2  36986  fnejoin2  36988  tailfb  36996  axuntco  37098  dfttc4lem2  37148  knoppcnlem9  37198  isinf2  38159  pibt2  38171  wl-ax13lem1  38248  wl-sbcom2d  38324  poimirlem25  38394  poimirlem27  38396  heicant  38404  itg2addnclem  38420  sdclem1  38493  fdc  38495  istotbnd3  38521  sstotbnd2  38524  prdsbnd2  38545  heibor1lem  38559  heiborlem1  38561  heiborlem10  38570  heibor  38571  riscer  38738  divrngidl  38778  iss2  39092  eqvreldisj  39446  disjlem17  39650  prtlem17  39749  ax12eq  39814  ax12el  39815  ax12inda  39821  ax12v2-o  39822  osumcllem8N  40836  pexmidlem5N  40847  mapdrvallem2  42518  sn-sup2  43379  onexomgt  44082  onexoegt  44085  omabs2  44173  clcnvlem  44463  onfrALT  45372  chordthmALT  45755  relpmin  45775  relpfrlem  45776  modelaxreplem1  45801  wfac8prim  45825  snelmap  45916  ssnnf1octb  46026  choicefi  46031  mapss2  46036  difmap  46037  axccdom  46052  infxrlesupxr  46264  inficc  46364  fsumnncl  46402  stoweidlem43  46871  stoweidlem48  46876  stoweidlem57  46885  stoweidlem60  46888  qndenserrnopn  47126  issalnnd  47173  subsaliuncl  47186  sge0cl  47209  nnfoctbdj  47284  ismeannd  47295  caragenunicl  47352  isomennd  47359  ovn0lem  47393  ovnsubaddlem2  47399  hspdifhsp  47444  hspmbllem3  47456  smflimlem6  47604  smfpimbor1lem1  47626  smfpimcc  47636  smfsuplem2  47640  rlimdmafv  48065  dfatcolem  48143  rlimdmafv2  48146  grimuhgr  48803  grimcnv  48804  grimco  48805  uhgrimedgi  48806  isuspgrim0  48810  gricushgr  48833  gricsym  48837  uhgrimisgrgric  48847  clnbgrgrimlem  48849  clnbgrgrim  48850  grimedg  48851  grtriprop  48857  usgrgrtrirex  48866  isubgr3stgrlem3  48884  uspgrlim  48908  grlimprclnbgredg  48913  grlimgredgex  48916  grlimgrtri  48919  xpco2  49785  opnneilv  49835  thincciso  50379