MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exlimdv Structured version   Visualization version   GIF version

Theorem exlimdv 2024
Description: Deduction form of Theorem 19.23 of [Margaris] p. 90, see 19.23 2248. (Contributed by NM, 27-Apr-1994.) Remove dependencies on ax-6 2069, ax-7 2105. (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
StepHypRef Expression
1 exlimdv.1 . . 3 (𝜑 → (𝜓𝜒))
21eximdv 2008 . 2 (𝜑 → (∃𝑥𝜓 → ∃𝑥𝜒))
3 ax5e 2003 . 2 (∃𝑥𝜒𝜒)
42, 3syl6 35 1 (𝜑 → (∃𝑥𝜓𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wex 1859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001
This theorem depends on definitions:  df-bi 198  df-ex 1860
This theorem is referenced by:  exlimdvv  2025  exlimddv  2026  ax13lem1  2424  ax13  2425  nfeqf  2471  axc15  2473  sbcom2  2608  sssn  4558  elpreqprb  4601  reusv2lem2  5081  ralxfr2d  5092  euotd  5181  wefrc  5318  wereu2  5321  releldmb  5575  relelrnb  5576  elresOLD  5653  iss  5666  onfr  5989  dffv2  6502  dff3  6604  elunirn  6743  fsnex  6772  f1prex  6773  isomin  6821  isofrlem  6824  ovmpt4g  7023  soex  7349  f1oweALT  7392  op1steq  7452  fo2ndf  7528  mpt2xopynvov0g  7585  reldmtpos  7605  rntpos  7610  wfrlem12  7672  wfrlem17  7677  erdisj  8039  map0g  8143  resixpfo  8193  domdifsn  8292  xpdom3  8307  domunsncan  8309  enfixsn  8318  fodomr  8360  mapdom2  8380  mapdom3  8381  phplem4  8391  php3  8395  sucdom2  8405  pssnn  8427  ssfi  8429  domfi  8430  findcard2  8449  ac6sfi  8453  isfinite2  8467  xpfi  8480  domunfican  8482  fiint  8486  fodomfib  8489  mapfien2  8563  marypha1lem  8588  ordiso  8670  hartogslem1  8696  brwdom2  8727  wdomtr  8729  brwdom3  8736  unwdomg  8738  xpwdomg  8739  unxpwdom2  8742  inf3lem2  8783  epfrs  8864  tcmin  8874  cplem1  9009  pm54.43  9119  dfac8alem  9145  dfac8b  9147  dfac8clem  9148  ac10ct  9150  acni2  9162  acndom  9167  numwdom  9175  wdomfil  9177  wdomnumr  9180  iunfictbso  9230  dfac2b  9246  dfac2OLD  9248  dfac9  9253  kmlem13  9279  cdainf  9309  fictb  9362  cfeq0  9373  cff1  9375  cfflb  9376  cofsmo  9386  cfsmolem  9387  coftr  9390  infpssr  9425  fin4en1  9426  fin23lem7  9433  isf34lem4  9494  axcc3  9555  domtriomlem  9559  axdc2lem  9565  axdc3lem2  9568  axdc3lem4  9570  axdc4lem  9572  ac6num  9596  ttukeylem6  9631  ttukeyg  9634  fodomb  9643  iundom2g  9657  alephreg  9699  fpwwe2lem11  9757  fpwwe2lem12  9758  canthp1  9771  pwfseq  9781  gruen  9929  grudomon  9934  gruina  9935  grur1  9937  ltexnq  10092  ltbtwnnq  10095  genpn0  10120  psslinpr  10148  prlem934  10150  ltaddpr  10151  ltexprlem2  10154  ltexprlem6  10158  ltexprlem7  10159  reclem2pr  10165  reclem4pr  10167  suplem1pr  10169  negn0  10754  sup2  11274  supaddc  11285  supmul1  11287  zsupss  12016  fiinfnf1o  13378  hasheqf1oi  13380  hashfun  13461  hashf1  13478  rtrclreclem3  14043  rlimdm  14525  climcau  14644  caucvgb  14653  summolem2  14690  zsum  14692  sumz  14696  fsumf1o  14697  fsumss  14699  fsumcl2lem  14705  fsumadd  14713  fsummulc2  14758  fsumconst  14764  fsumrelem  14781  ntrivcvg  14870  prodmolem2  14906  zprod  14908  prod1  14915  fprodf1o  14917  fprodss  14919  fprodcl2lem  14921  fprodmul  14931  fproddiv  14932  fprodconst  14949  fprodn0  14950  ruclem13  15211  4sqlem12  15897  vdwapun  15915  vdwlem9  15930  vdwlem10  15931  ramz  15966  ramub1  15969  firest  16318  mremre  16489  isacs2  16538  iscatd2  16566  sscfn1  16701  sscfn2  16702  gsumval2a  17504  symggen  18111  cyggex2  18519  gsumval3  18529  gsumzres  18531  gsumzcl2  18532  gsumzf1o  18534  gsumzaddlem  18542  gsumconst  18555  gsumzmhm  18558  gsumzoppg  18565  gsum2d2  18594  pgpfac1lem5  18700  ablfaclem3  18708  lss0cl  19171  lspsnat  19373  cnsubrg  20034  gsumfsum  20041  obslbs  20305  lmiclbs  20407  lmisfree  20412  mdetdiaglem  20636  mdet0  20644  eltg3  21001  tgtop  21012  tgidm  21019  ppttop  21046  toponmre  21132  tgrest  21198  neitr  21219  tgcn  21291  cmpsublem  21437  cmpsub  21438  iunconnlem  21465  unconn  21467  1stcfb  21483  2ndcctbss  21493  2ndcdisj  21494  1stcelcls  21499  1stccnp  21500  locfincmp  21564  comppfsc  21570  1stckgen  21592  ptuni2  21614  ptbasfi  21619  ptpjopn  21650  ptclsg  21653  ptcnp  21660  prdstopn  21666  txindis  21672  txtube  21678  txcmplem1  21679  txcmplem2  21680  xkococnlem  21697  txconn  21727  trfbas2  21881  filtop  21893  filconn  21921  filssufilg  21949  fmfnfm  21996  ufldom  22000  hauspwpwf1  22025  alexsubALTlem3  22087  alexsubALT  22089  ptcmplem2  22091  tmdgsum2  22134  tgptsmscld  22188  ustfilxp  22250  xbln0  22453  opnreen  22868  metdsre  22890  cnheibor  22988  phtpc01  23029  cfilfcls  23306  cmetcaulem  23320  iscmet3  23325  ovolctb  23494  ovoliunlem3  23508  ovoliunnul  23511  ovolicc2lem5  23525  ovolicc2  23526  dyadmbl  23604  vitali  23617  itg11  23695  bddmulibl  23842  perfdvf  23904  dvcnp2  23920  dvlip  23993  dvne0  24011  fta1g  24164  fta1  24300  ulmcau  24386  pserulm  24413  wilthlem2  25032  dchrvmasumif  25429  rpvmasum2  25438  dchrisum0re  25439  dchrisum0lem3  25445  dchrisum0  25446  dchrmusum  25450  dchrvmasum  25451  axcontlem10  26090  usgr1v0e  26457  wlkiswwlks  27026  wlkiswwlkupgr  27028  wlklnwwlkn  27034  wlklnwwlknupgr  27036  umgrwwlks2on  27121  elwwlks2  27131  elwspths2spth  27132  clwlkclwwlklem3  27167  clwlkclwwlkfo  27175  clwlksfoclwwlkOLD  27260  frgr3vlem2  27472  spansncvi  28862  reff  30254  locfinreflem  30255  cmpcref  30265  fmcncfil  30325  volmeas  30642  omssubadd  30710  bnj849  31340  derangenlem  31498  cvmsss2  31601  cvmopnlem  31605  cvmfolem  31606  cvmliftmolem2  31609  cvmliftlem15  31625  cvmlift2lem10  31639  cvmlift3lem8  31653  fundmpss  32008  frpomin  32081  frmin  32085  frrlem11  32135  nocvxmin  32237  fnessref  32695  refssfne  32696  neibastop2lem  32698  neibastop2  32699  fnemeet2  32705  fnejoin2  32707  tailfb  32715  knoppcnlem9  32830  wl-ax13lem1  33624  wl-sbcom2d  33677  matunitlindflem2  33738  poimirlem25  33766  poimirlem27  33768  heicant  33776  itg2addnclem  33792  sdclem1  33869  fdc  33871  istotbnd3  33900  sstotbnd2  33903  prdsbnd2  33924  heibor1lem  33938  heiborlem1  33940  heiborlem10  33949  heibor  33950  riscer  34117  divrngidl  34157  iss2  34444  prtlem17  34674  ax12eq  34739  ax12el  34740  ax12inda  34746  ax12v2-o  34747  osumcllem8N  35762  pexmidlem5N  35773  mapdrvallem2  37444  clcnvlem  38448  onfrALT  39280  chordthmALT  39681  snelmap  39765  ssnnf1octb  39889  choicefi  39897  mapss2  39902  difmap  39904  axccdom  39921  infxrlesupxr  40160  inficc  40259  fsumnncl  40301  stoweidlem43  40757  stoweidlem48  40762  stoweidlem57  40771  stoweidlem60  40774  qndenserrnopn  41015  issalnnd  41060  subsaliuncl  41073  sge0cl  41095  nnfoctbdj  41170  ismeannd  41181  caragenunicl  41238  isomennd  41245  ovn0lem  41279  ovnsubaddlem2  41285  hspdifhsp  41330  hspmbllem3  41342  smflimlem6  41484  smfpimbor1lem1  41505  smfpimcc  41514  smfsuplem2  41518  rlimdmafv  41784  dfatcolem  41862  rlimdmafv2  41865  mgmpropd  42361  c0snmgmhm  42500
  Copyright terms: Public domain W3C validator