Theorem exlimdv 1933

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

Syntax hints:   → wi 4  ∃wex 1779

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

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

This theorem is referenced by:  exlimdvv  1934  exlimddv  1935  ax13lem1  2372  ax13  2373  nfeqf  2379  axc15  2420  sssn  4790  elpreqprb  4832  reusv2lem2  5354  ralxfr2d  5365  euotd  5473  wefrc  5632  wereu2  5635  releldmb  5910  relelrnb  5911  iss  6006  frpomin  6313  onfr  6371  dffv2  6956  dff3  7072  elunirn  7225  fsnex  7258  f1prex  7259  isomin  7312  isofrlem  7315  ovmpt4g  7536  soex  7897  f1oweALT  7951  op1steq  8012  fo2ndf  8100  frxp3  8130  mpoxopynvov0g  8193  reldmtpos  8213  rntpos  8218  frrlem10  8274  fprresex  8289  erdisj  8728  map0g  8857  resixpfo  8909  domdifsn  9024  xpdom3  9039  domunsncan  9041  enfixsn  9050  fodomr  9092  mapdom2  9112  mapdom3  9113  rexdif1en  9122  pssnn  9132  ssfiALT  9138  domfi  9153  sucdom2  9167  phplem2  9169  php3  9173  0sdom1dom  9185  sdom1  9189  1sdom2dom  9194  ac6sfi  9231  isfinite2  9245  xpfiOLD  9270  domunfican  9272  fiint  9277  fiintOLD  9278  fodomfir  9279  fodomfib  9280  fodomfibOLD  9282  mapfien2  9360  marypha1lem  9384  ordiso  9469  hartogslem1  9495  brwdom2  9526  wdomtr  9528  brwdom3  9535  unwdomg  9537  xpwdomg  9538  unxpwdom2  9541  inf3lem2  9582  ttrclss  9673  dmttrcl  9674  rnttrcl  9675  ttrclselem2  9679  epfrs  9684  tcmin  9694  frmin  9702  cplem1  9842  pm54.43  9954  dfac8alem  9982  dfac8b  9984  dfac8clem  9985  ac10ct  9987  acni2  9999  acndom  10004  numwdom  10012  wdomfil  10014  wdomnumr  10017  iunfictbso  10067  dfac2b  10084  dfac9  10090  kmlem13  10116  djuinf  10142  fictb  10197  cfeq0  10209  cff1  10211  cfflb  10212  cofsmo  10222  cfsmolem  10223  coftr  10226  infpssr  10261  fin4en1  10262  fin23lem7  10269  isf34lem4  10330  axcc3  10391  domtriomlem  10395  axdc2lem  10401  axdc3lem2  10404  axdc3lem4  10406  axdc4lem  10408  ac6num  10432  ttukeylem6  10467  ttukeyg  10470  fodomb  10479  iundom2g  10493  alephreg  10535  fpwwe2lem10  10593  fpwwe2lem11  10594  canthp1  10607  pwfseq  10617  gruen  10765  grudomon  10770  gruina  10771  grur1  10773  ltexnq  10928  ltbtwnnq  10931  genpn0  10956  psslinpr  10984  prlem934  10986  ltaddpr  10987  ltexprlem2  10990  ltexprlem6  10994  ltexprlem7  10995  reclem2pr  11001  reclem4pr  11003  suplem1pr  11005  negn0  11607  sup2  12139  supaddc  12150  supmul1  12152  zsupss  12896  fiinfnf1o  14315  hasheqf1oi  14316  hashfun  14402  hashf1  14422  hash3tpexb  14459  rtrclreclem3  15026  rlimdm  15517  climcau  15637  caucvgb  15646  summolem2  15682  zsum  15684  sumz  15688  fsumf1o  15689  fsumss  15691  fsumcl2lem  15697  fsumadd  15706  fsummulc2  15750  fsumconst  15756  fsumrelem  15773  ntrivcvg  15863  prodmolem2  15901  zprod  15903  prod1  15910  fprodf1o  15912  fprodss  15914  fprodcl2lem  15916  fprodmul  15926  fproddiv  15927  fprodconst  15944  fprodn0  15945  ruclem13  16210  4sqlem12  16927  vdwapun  16945  vdwlem9  16960  vdwlem10  16961  ramz  16996  ramub1  16999  firest  17395  mremre  17565  isacs2  17614  iscatd2  17642  cicsym  17766  sscfn1  17779  sscfn2  17780  initoeu2  17978  mgmpropd  18578  gsumval2a  18612  symggen  19400  cyggex2  19827  gsumval3  19837  gsumzres  19839  gsumzcl2  19840  gsumzf1o  19842  gsumzaddlem  19851  gsumconst  19864  gsumzmhm  19867  gsumzoppg  19874  gsum2d2  19904  pgpfac1lem5  20011  ablfaclem3  20019  c0snmgmhm  20371  lss0cl  20853  lspsnat  21055  cnsubrg  21344  gsumfsum  21351  obslbs  21639  lmiclbs  21746  lmisfree  21751  mdetdiaglem  22485  mdet0  22493  eltg3  22849  tgtop  22860  tgidm  22867  ppttop  22894  toponmre  22980  tgrest  23046  neitr  23067  tgcn  23139  cmpsublem  23286  cmpsub  23287  iunconnlem  23314  unconn  23316  1stcfb  23332  2ndcctbss  23342  2ndcdisj  23343  1stcelcls  23348  1stccnp  23349  locfincmp  23413  comppfsc  23419  1stckgen  23441  ptuni2  23463  ptbasfi  23468  ptpjopn  23499  ptclsg  23502  ptcnp  23509  prdstopn  23515  txindis  23521  txtube  23527  txcmplem1  23528  txcmplem2  23529  xkococnlem  23546  txconn  23576  trfbas2  23730  filtop  23742  filconn  23770  filssufilg  23798  fmfnfm  23845  ufldom  23849  hauspwpwf1  23874  alexsubALTlem3  23936  alexsubALT  23938  ptcmplem2  23940  tmdgsum2  23983  tgptsmscld  24038  ustfilxp  24100  xbln0  24302  opnreen  24720  metdsre  24742  cnheibor  24854  phtpc01  24895  cfilfcls  25174  cmetcaulem  25188  iscmet3  25193  ovolctb  25391  ovoliunlem3  25405  ovoliunnul  25408  ovolicc2lem5  25422  ovolicc2  25423  dyadmbl  25501  vitali  25514  itg11  25592  bddmulibl  25740  perfdvf  25804  dvcnp2  25821  dvcnp2OLD  25822  dvlip  25898  dvne0  25916  fta1g  26075  fta1  26216  ulmcau  26304  pserulm  26331  wilthlem2  26979  dchrvmasumif  27414  rpvmasum2  27423  dchrisum0re  27424  dchrisum0lem3  27430  dchrisum0  27431  dchrmusum  27435  dchrvmasum  27436  noinfno  27630  nocvxmin  27690  sltlpss  27819  axcontlem10  28900  usgr1v0e  29253  wlkiswwlks  29806  wlkiswwlkupgr  29808  wlklnwwlkn  29814  wlklnwwlknupgr  29816  umgrwwlks2on  29887  elwwlks2  29896  elwspths2spth  29897  clwlkclwwlklem3  29930  clwlkclwwlkfo  29938  frgr3vlem2  30203  spansncvi  31581  2ndresdju  32573  fnpreimac  32595  gsumwrd2dccatlem  33006  qsidomlem2  33424  reff  33829  locfinreflem  33830  cmpcref  33840  fmcncfil  33921  volmeas  34221  omssubadd  34291  bnj849  34915  acycgrislfgr  35139  derangenlem  35158  cvmsss2  35261  cvmopnlem  35265  cvmfolem  35266  cvmliftmolem2  35269  cvmliftlem15  35285  cvmlift2lem10  35299  cvmlift3lem8  35313  satfdmlem  35355  sat1el2xp  35366  fmlasuc  35373  fundmpss  35754  fnessref  36345  refssfne  36346  neibastop2lem  36348  neibastop2  36349  fnemeet2  36355  fnejoin2  36357  tailfb  36365  knoppcnlem9  36489  isinf2  37393  pibt2  37405  wl-ax13lem1  37482  wl-sbcom2d  37549  matunitlindflem2  37611  poimirlem25  37639  poimirlem27  37641  heicant  37649  itg2addnclem  37665  sdclem1  37737  fdc  37739  istotbnd3  37765  sstotbnd2  37768  prdsbnd2  37789  heibor1lem  37803  heiborlem1  37805  heiborlem10  37814  heibor  37815  riscer  37982  divrngidl  38022  iss2  38326  eqvreldisj  38605  disjlem17  38791  prtlem17  38869  ax12eq  38934  ax12el  38935  ax12inda  38941  ax12v2-o  38942  osumcllem8N  39957  pexmidlem5N  39968  mapdrvallem2  41639  sn-sup2  42479  onexomgt  43230  onexoegt  43233  omabs2  43321  clcnvlem  43612  onfrALT  44539  chordthmALT  44922  relpmin  44942  relpfrlem  44943  modelaxreplem1  44968  wfac8prim  44992  snelmap  45076  ssnnf1octb  45188  choicefi  45194  mapss2  45199  difmap  45201  axccdom  45216  infxrlesupxr  45432  inficc  45532  fsumnncl  45570  stoweidlem43  46041  stoweidlem48  46046  stoweidlem57  46055  stoweidlem60  46058  qndenserrnopn  46296  issalnnd  46343  subsaliuncl  46356  sge0cl  46379  nnfoctbdj  46454  ismeannd  46465  caragenunicl  46522  isomennd  46529  ovn0lem  46563  ovnsubaddlem2  46569  hspdifhsp  46614  hspmbllem3  46626  smflimlem6  46774  smfpimbor1lem1  46796  smfpimcc  46806  smfsuplem2  46810  rlimdmafv  47178  dfatcolem  47256  rlimdmafv2  47259  grimuhgr  47887  grimcnv  47888  grimco  47889  uhgrimedgi  47890  isuspgrim0  47894  gricushgr  47917  gricsym  47921  uhgrimisgrgric  47931  clnbgrgrimlem  47933  clnbgrgrim  47934  grimedg  47935  grtriprop  47940  usgrgrtrirex  47949  isubgr3stgrlem3  47967  uspgrlim  47991  grlimgrtri  47995  xpco2  48845  opnneilv  48897  thincciso  49442