Theorem exlimdv 1934

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

Syntax hints:   → wi 4  ∃wex 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

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

This theorem is referenced by:  exlimdvv  1935  exlimddv  1936  ax13lem1  2378  ax13  2379  nfeqf  2385  axc15  2426  sssn  4782  elpreqprb  4824  reusv2lem2  5344  ralxfr2d  5355  euotd  5461  wefrc  5618  wereu2  5621  releldmb  5895  relelrnb  5896  iss  5994  frpomin  6298  onfr  6356  dffv2  6929  dff3  7045  elunirn  7197  fsnex  7229  f1prex  7230  isomin  7283  isofrlem  7286  ovmpt4g  7505  soex  7863  f1oweALT  7916  op1steq  7977  fo2ndf  8063  frxp3  8093  mpoxopynvov0g  8156  reldmtpos  8176  rntpos  8181  frrlem10  8237  fprresex  8252  erdisj  8692  map0g  8822  resixpfo  8874  domdifsn  8988  xpdom3  9003  domunsncan  9005  enfixsn  9014  fodomr  9056  mapdom2  9076  mapdom3  9077  rexdif1en  9085  pssnn  9093  ssfiALT  9098  domfi  9113  sucdom2  9127  phplem2  9129  php3  9133  0sdom1dom  9146  sdom1  9150  1sdom2dom  9154  ac6sfi  9184  isfinite2  9198  domunfican  9222  fiint  9227  fodomfir  9228  fodomfib  9229  fodomfibOLD  9231  mapfien2  9312  marypha1lem  9336  ordiso  9421  hartogslem1  9447  brwdom2  9478  wdomtr  9480  brwdom3  9487  unwdomg  9489  xpwdomg  9490  unxpwdom2  9493  inf3lem2  9538  ttrclss  9629  dmttrcl  9630  rnttrcl  9631  ttrclselem2  9635  epfrs  9640  tcmin  9648  frmin  9661  cplem1  9801  pm54.43  9913  dfac8alem  9939  dfac8b  9941  dfac8clem  9942  ac10ct  9944  acni2  9956  acndom  9961  numwdom  9969  wdomfil  9971  wdomnumr  9974  iunfictbso  10024  dfac2b  10041  dfac9  10047  kmlem13  10073  djuinf  10099  fictb  10154  cfeq0  10166  cff1  10168  cfflb  10169  cofsmo  10179  cfsmolem  10180  coftr  10183  infpssr  10218  fin4en1  10219  fin23lem7  10226  isf34lem4  10287  axcc3  10348  domtriomlem  10352  axdc2lem  10358  axdc3lem2  10361  axdc3lem4  10363  axdc4lem  10365  ac6num  10389  ttukeylem6  10424  ttukeyg  10427  fodomb  10436  iundom2g  10450  alephreg  10493  fpwwe2lem10  10551  fpwwe2lem11  10552  canthp1  10565  pwfseq  10575  gruen  10723  grudomon  10728  gruina  10729  grur1  10731  ltexnq  10886  ltbtwnnq  10889  genpn0  10914  psslinpr  10942  prlem934  10944  ltaddpr  10945  ltexprlem2  10948  ltexprlem6  10952  ltexprlem7  10953  reclem2pr  10959  reclem4pr  10961  suplem1pr  10963  negn0  11566  sup2  12098  supaddc  12109  supmul1  12111  zsupss  12850  fiinfnf1o  14273  hasheqf1oi  14274  hashfun  14360  hashf1  14380  hash3tpexb  14417  rtrclreclem3  14983  rlimdm  15474  climcau  15594  caucvgb  15603  summolem2  15639  zsum  15641  sumz  15645  fsumf1o  15646  fsumss  15648  fsumcl2lem  15654  fsumadd  15663  fsummulc2  15707  fsumconst  15713  fsumrelem  15730  ntrivcvg  15820  prodmolem2  15858  zprod  15860  prod1  15867  fprodf1o  15869  fprodss  15871  fprodcl2lem  15873  fprodmul  15883  fproddiv  15884  fprodconst  15901  fprodn0  15902  ruclem13  16167  4sqlem12  16884  vdwapun  16902  vdwlem9  16917  vdwlem10  16918  ramz  16953  ramub1  16956  firest  17352  mremre  17523  isacs2  17576  iscatd2  17604  cicsym  17728  sscfn1  17741  sscfn2  17742  initoeu2  17940  mgmpropd  18576  gsumval2a  18610  symggen  19399  cyggex2  19826  gsumval3  19836  gsumzres  19838  gsumzcl2  19839  gsumzf1o  19841  gsumzaddlem  19850  gsumconst  19863  gsumzmhm  19866  gsumzoppg  19873  gsum2d2  19903  pgpfac1lem5  20010  ablfaclem3  20018  c0snmgmhm  20398  lss0cl  20898  lspsnat  21100  cnsubrg  21382  gsumfsum  21389  obslbs  21685  lmiclbs  21792  lmisfree  21797  mdetdiaglem  22542  mdet0  22550  eltg3  22906  tgtop  22917  tgidm  22924  ppttop  22951  toponmre  23037  tgrest  23103  neitr  23124  tgcn  23196  cmpsublem  23343  cmpsub  23344  iunconnlem  23371  unconn  23373  1stcfb  23389  2ndcctbss  23399  2ndcdisj  23400  1stcelcls  23405  1stccnp  23406  locfincmp  23470  comppfsc  23476  1stckgen  23498  ptuni2  23520  ptbasfi  23525  ptpjopn  23556  ptclsg  23559  ptcnp  23566  prdstopn  23572  txindis  23578  txtube  23584  txcmplem1  23585  txcmplem2  23586  xkococnlem  23603  txconn  23633  trfbas2  23787  filtop  23799  filconn  23827  filssufilg  23855  fmfnfm  23902  ufldom  23906  hauspwpwf1  23931  alexsubALTlem3  23993  alexsubALT  23995  ptcmplem2  23997  tmdgsum2  24040  tgptsmscld  24095  ustfilxp  24157  xbln0  24358  opnreen  24776  metdsre  24798  cnheibor  24910  phtpc01  24951  cfilfcls  25230  cmetcaulem  25244  iscmet3  25249  ovolctb  25447  ovoliunlem3  25461  ovoliunnul  25464  ovolicc2lem5  25478  ovolicc2  25479  dyadmbl  25557  vitali  25570  itg11  25648  bddmulibl  25796  perfdvf  25860  dvcnp2  25877  dvcnp2OLD  25878  dvlip  25954  dvne0  25972  fta1g  26131  fta1  26272  ulmcau  26360  pserulm  26387  wilthlem2  27035  dchrvmasumif  27470  rpvmasum2  27479  dchrisum0re  27480  dchrisum0lem3  27486  dchrisum0  27487  dchrmusum  27491  dchrvmasum  27492  noinfno  27686  nobdaymin  27749  ltslpss  27904  axcontlem10  29046  usgr1v0e  29399  wlkiswwlks  29949  wlkiswwlkupgr  29951  wlklnwwlkn  29957  wlklnwwlknupgr  29959  usgrwwlks2on  30031  umgrwwlks2on  30032  elwwlks2  30042  elwspths2spth  30043  clwlkclwwlklem3  30076  clwlkclwwlkfo  30084  frgr3vlem2  30349  spansncvi  31727  2ndresdju  32727  fnpreimac  32749  gsumwrd2dccatlem  33159  qsidomlem2  33534  reff  33996  locfinreflem  33997  cmpcref  34007  fmcncfil  34088  volmeas  34388  omssubadd  34457  bnj849  35081  r1filimi  35259  acycgrislfgr  35346  derangenlem  35365  cvmsss2  35468  cvmopnlem  35472  cvmfolem  35473  cvmliftmolem2  35476  cvmliftlem15  35492  cvmlift2lem10  35506  cvmlift3lem8  35520  satfdmlem  35562  sat1el2xp  35573  fmlasuc  35580  fundmpss  35961  fnessref  36551  refssfne  36552  neibastop2lem  36554  neibastop2  36555  fnemeet2  36561  fnejoin2  36563  tailfb  36571  knoppcnlem9  36701  isinf2  37610  pibt2  37622  wl-ax13lem1  37699  wl-sbcom2d  37766  matunitlindflem2  37818  poimirlem25  37846  poimirlem27  37848  heicant  37856  itg2addnclem  37872  sdclem1  37944  fdc  37946  istotbnd3  37972  sstotbnd2  37975  prdsbnd2  37996  heibor1lem  38010  heiborlem1  38012  heiborlem10  38021  heibor  38022  riscer  38189  divrngidl  38229  iss2  38537  eqvreldisj  38871  disjlem17  39058  prtlem17  39136  ax12eq  39201  ax12el  39202  ax12inda  39208  ax12v2-o  39209  osumcllem8N  40223  pexmidlem5N  40234  mapdrvallem2  41905  sn-sup2  42746  onexomgt  43483  onexoegt  43486  omabs2  43574  clcnvlem  43864  onfrALT  44790  chordthmALT  45173  relpmin  45193  relpfrlem  45194  modelaxreplem1  45219  wfac8prim  45243  snelmap  45327  ssnnf1octb  45438  choicefi  45444  mapss2  45449  difmap  45451  axccdom  45466  infxrlesupxr  45680  inficc  45780  fsumnncl  45818  stoweidlem43  46287  stoweidlem48  46292  stoweidlem57  46301  stoweidlem60  46304  qndenserrnopn  46542  issalnnd  46589  subsaliuncl  46602  sge0cl  46625  nnfoctbdj  46700  ismeannd  46711  caragenunicl  46768  isomennd  46775  ovn0lem  46809  ovnsubaddlem2  46815  hspdifhsp  46860  hspmbllem3  46872  smflimlem6  47020  smfpimbor1lem1  47042  smfpimcc  47052  smfsuplem2  47056  rlimdmafv  47423  dfatcolem  47501  rlimdmafv2  47504  grimuhgr  48133  grimcnv  48134  grimco  48135  uhgrimedgi  48136  isuspgrim0  48140  gricushgr  48163  gricsym  48167  uhgrimisgrgric  48177  clnbgrgrimlem  48179  clnbgrgrim  48180  grimedg  48181  grtriprop  48187  usgrgrtrirex  48196  isubgr3stgrlem3  48214  uspgrlim  48238  grlimprclnbgredg  48243  grlimgredgex  48246  grlimgrtri  48249  xpco2  49102  opnneilv  49154  thincciso  49698