Theorem exlimdv 1963

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 1997, ax-7 2038. (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 1947	. 2 ⊢ (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
3		ax5e 1942	. 2 ⊢ (∃𝑥𝜒 → 𝜒)
4	2, 3	syl6 36	1 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))

Syntax hints:   → wi 4  ∃wex 1809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-ex 1810

This theorem is referenced by:  exlimdvv  1964  exlimddv  1965  ax13lem1  2406  ax13  2407  nfeqf  2413  axc15  2454  sssn  4793  elpreqprb  4834  reusv2lem2  5372  ralxfr2d  5383  euotd  5498  wefrc  5657  wereu2  5660  releldmb  5938  relelrnb  5939  iss  6039  frpomin  6343  onfr  6402  dffv2  6978  dff3  7097  elunirn  7251  fsnex  7283  f1prex  7284  isomin  7337  isofrlem  7340  ovmpt4g  7559  soex  7919  f1oweALT  7970  op1steq  8031  fo2ndf  8117  frxp3  8148  mpoxopynvov0g  8211  reldmtpos  8231  rntpos  8236  frrlem10  8293  fprresex  8308  erdisj  8753  map0g  8883  resixpfo  8935  domdifsn  9049  xpdom3  9064  domunsncan  9066  enfixsn  9075  fodomr  9117  mapdom2  9137  mapdom3  9138  rexdif1en  9146  pssnn  9154  ssfiALT  9159  domfi  9174  sucdom2  9188  phplem2  9190  php3  9194  0sdom1dom  9207  sdom1  9211  1sdom2dom  9215  ac6sfi  9245  isfinite2  9259  domunfican  9282  fiint  9287  fodomfir  9288  fodomfib  9289  mapfien2  9370  marypha1lem  9394  ordiso  9479  hartogslem1  9505  brwdom2  9536  wdomtr  9538  brwdom3  9545  unwdomg  9547  xpwdomg  9548  unxpwdom2  9551  inf3lem2  9599  ttrclss  9690  dmttrcl  9691  rnttrcl  9692  ttrclselem2  9696  epfrs  9701  tcmin  9709  frmin  9722  cplem1  9876  pm54.43  9988  dfac8alem  10014  dfac8b  10016  dfac8clem  10017  ac10ct  10019  acni2  10031  acndom  10036  numwdom  10044  wdomfil  10046  wdomnumr  10049  iunfictbso  10099  dfac2b  10115  dfac9  10121  kmlem13  10147  djuinf  10173  fictb  10228  cfeq0  10241  cff1  10243  cfflb  10244  cofsmo  10254  cfsmolem  10255  coftr  10258  infpssr  10293  fin4en1  10294  fin23lem7  10301  isf34lem4  10362  axcc3  10423  domtriomlem  10427  axdc2lem  10433  axdc3lem2  10436  axdc3lem4  10438  axdc4lem  10440  ac6num  10464  ttukeylem6  10499  ttukeyg  10502  fodomb  10511  iundom2g  10525  alephreg  10568  fpwwe2lem10  10626  fpwwe2lem11  10627  canthp1  10640  pwfseq  10650  gruen  10798  grudomon  10803  gruina  10804  grur1  10806  ltexnq  10961  ltbtwnnq  10964  genpn0  10989  psslinpr  11017  prlem934  11019  ltaddpr  11020  ltexprlem2  11023  ltexprlem6  11027  ltexprlem7  11028  reclem2pr  11034  reclem4pr  11036  suplem1pr  11038  negn0  11644  sup2  12172  supaddc  12183  supmul1  12185  zsupss  12962  fiinfnf1o  14388  hasheqf1oi  14389  hashfun  14476  hashf1  14496  hash3tpexb  14533  rtrclreclem3  15099  rlimdm  15604  climcau  15724  caucvgb  15733  summolem2  15769  zsum  15771  sumz  15775  fsumf1o  15776  fsumss  15778  fsumcl2lem  15784  fsumadd  15793  fsummulc2  15837  fsumconst  15843  fsumrelem  15861  ntrivcvg  15953  prodmolem2  15991  zprod  15993  prod1  16000  fprodf1o  16002  fprodss  16004  fprodcl2lem  16006  fprodmul  16016  fproddiv  16017  fprodconst  16034  fprodn0  16035  ruclem13  16299  4sqlem12  17017  vdwapun  17035  vdwlem9  17050  vdwlem10  17051  ramz  17086  ramub1  17089  firest  17486  mremre  17657  isacs2  17710  iscatd2  17738  cicsym  17862  sscfn1  17875  sscfn2  17876  initoeu2  18074  mgmpropd  18710  gsumval2a  18744  symggen  19541  cyggex2  19968  gsumval3  19978  gsumzres  19980  gsumzcl2  19981  gsumzf1o  19983  gsumzaddlem  19992  gsumconst  20005  gsumzmhm  20008  gsumzoppg  20015  gsum2d2  20045  pgpfac1lem5  20152  ablfaclem3  20160  c0snmgmhm  20545  lss0cl  21049  lspsnat  21250  qsidomlem2  21462  cnsubrg  21558  gsumfsum  21565  obslbs  21861  lmiclbs  21968  lmisfree  21973  mdetdiaglem  22736  mdet0  22744  eltg3  23100  tgtop  23111  tgidm  23118  ppttop  23145  toponmre  23231  tgrest  23297  neitr  23318  tgcn  23390  cmpsublem  23537  cmpsub  23538  iunconnlem  23565  unconn  23567  1stcfb  23583  2ndcctbss  23593  2ndcdisj  23594  1stcelcls  23599  1stccnp  23600  locfincmp  23664  comppfsc  23670  1stckgen  23692  ptuni2  23714  ptbasfi  23719  ptpjopn  23750  ptclsg  23753  ptcnp  23760  prdstopn  23766  txindis  23772  txtube  23778  txcmplem1  23779  txcmplem2  23780  xkococnlem  23797  txconn  23827  trfbas2  23981  filtop  23993  filconn  24021  filssufilg  24049  fmfnfm  24096  ufldom  24100  hauspwpwf1  24125  alexsubALTlem3  24187  alexsubALT  24189  ptcmplem2  24191  tmdgsum2  24234  tgptsmscld  24289  ustfilxp  24351  xbln0  24552  opnreen  24970  metdsre  24992  cnheibor  25095  phtpc01  25136  cfilfcls  25414  cmetcaulem  25428  iscmet3  25433  ovolctb  25630  ovoliunlem3  25644  ovoliunnul  25647  ovolicc2lem5  25661  ovolicc2  25662  dyadmbl  25740  vitali  25753  itg11  25831  bddmulibl  25979  perfdvf  26043  dvcnp2  26060  dvlip  26133  dvne0  26151  fta1g  26308  fta1  26450  ulmcau  26539  pserulm  26566  wilthlem2  27214  dchrvmasumif  27648  rpvmasum2  27657  dchrisum0re  27658  dchrisum0lem3  27664  dchrisum0  27665  dchrmusum  27669  dchrvmasum  27670  noinfno  27863  nobdaymin  27927  ltslpss  28082  axcontlem10  29304  usgr1v0e  29657  wlkiswwlks  30206  wlkiswwlkupgr  30208  wlklnwwlkn  30214  wlklnwwlknupgr  30216  usgrwwlks2on  30288  umgrwwlks2on  30289  elwwlks2  30299  elwspths2spth  30300  clwlkclwwlklem3  30333  clwlkclwwlkfo  30341  frgr3vlem2  30606  spansncvi  31985  2ndresdju  32975  fnpreimac  32996  gsumwrd2dccatlem  33378  reff  34210  locfinreflem  34211  cmpcref  34221  fmcncfil  34302  volmeas  34602  omssubadd  34671  bnj849  35294  r1filimi  35478  kardfi  35564  onvfowev  35581  acycgrislfgr  35625  derangenlem  35644  cvmsss2  35747  cvmopnlem  35751  cvmfolem  35752  cvmliftmolem2  35755  cvmliftlem15  35771  cvmlift2lem10  35785  cvmlift3lem8  35799  satfdmlem  35841  sat1el2xp  35852  fmlasuc  35859  fundmpss  36240  fnessref  36849  refssfne  36850  neibastop2lem  36852  neibastop2  36853  fnemeet2  36859  fnejoin2  36861  tailfb  36869  axuntco  36971  dfttc4lem2  37021  knoppcnlem9  37071  isinf2  38032  pibt2  38044  wl-ax13lem1  38121  wl-sbcom2d  38197  matunitlindflem2  38249  poimirlem25  38277  poimirlem27  38279  heicant  38287  itg2addnclem  38303  sdclem1  38375  fdc  38377  istotbnd3  38403  sstotbnd2  38406  prdsbnd2  38427  heibor1lem  38441  heiborlem1  38443  heiborlem10  38452  heibor  38453  riscer  38620  divrngidl  38660  iss2  38974  eqvreldisj  39328  disjlem17  39532  prtlem17  39631  ax12eq  39696  ax12el  39697  ax12inda  39703  ax12v2-o  39704  osumcllem8N  40718  pexmidlem5N  40729  mapdrvallem2  42400  sn-sup2  43246  onexomgt  43951  onexoegt  43954  omabs2  44042  clcnvlem  44332  onfrALT  45241  chordthmALT  45624  relpmin  45644  relpfrlem  45645  modelaxreplem1  45670  wfac8prim  45694  snelmap  45785  ssnnf1octb  45895  choicefi  45900  mapss2  45905  difmap  45906  axccdom  45921  infxrlesupxr  46133  inficc  46233  fsumnncl  46271  stoweidlem43  46740  stoweidlem48  46745  stoweidlem57  46754  stoweidlem60  46757  qndenserrnopn  46995  issalnnd  47042  subsaliuncl  47055  sge0cl  47078  nnfoctbdj  47153  ismeannd  47164  caragenunicl  47221  isomennd  47228  ovn0lem  47262  ovnsubaddlem2  47268  hspdifhsp  47313  hspmbllem3  47325  smflimlem6  47473  smfpimbor1lem1  47495  smfpimcc  47505  smfsuplem2  47509  rlimdmafv  47897  dfatcolem  47975  rlimdmafv2  47978  grimuhgr  48635  grimcnv  48636  grimco  48637  uhgrimedgi  48638  isuspgrim0  48642  gricushgr  48665  gricsym  48669  uhgrimisgrgric  48679  clnbgrgrimlem  48681  clnbgrgrim  48682  grimedg  48683  grtriprop  48689  usgrgrtrirex  48698  isubgr3stgrlem3  48716  uspgrlim  48740  grlimprclnbgredg  48745  grlimgredgex  48748  grlimgrtri  48751  xpco2  49618  opnneilv  49670  thincciso  50214