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

Theorem sstr 3576
Description: Transitivity of subclasses. Theorem 6 of [Suppes] p. 23. (Contributed by NM, 5-Sep-2003.)
Assertion
Ref Expression
sstr ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)

Proof of Theorem sstr
StepHypRef Expression
1 sstr2 3575 . 2 (𝐴𝐵 → (𝐵𝐶𝐴𝐶))
21imp 444 1 ((𝐴𝐵𝐵𝐶) → 𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wss 3540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554
This theorem is referenced by:  sstrd  3578  sylan9ss  3581  ssdifss  3703  uneqin  3837  ssrnres  5491  relrelss  5576  fco  5971  fssres  5983  ssimaex  6173  dff3  6280  tpostpos2  7260  smores  7336  om00  7542  omeulem2  7550  pmss12g  7770  unblem1  8097  unblem2  8098  unblem3  8099  unblem4  8100  isfinite2  8103  cantnfval2  8449  cantnfle  8451  rankxplim3  8627  alephinit  8801  dfac12lem2  8849  ackbij1lem11  8935  cfeq0  8961  cfsuc  8962  cff1  8963  cflim2  8968  cfss  8970  cfslb2n  8973  cofsmo  8974  cfsmolem  8975  fin23lem34  9051  fin1a2lem13  9117  axdc3lem2  9156  axdclem  9224  pwcfsdom  9284  wunfi  9422  tskxpss  9473  tskcard  9482  suprzcl  11333  uzwo  11627  uzwo2  11628  infssuzle  11647  infssuzcl  11648  supxrbnd  12030  supxrgtmnf  12031  supxrre1  12032  supxrre2  12033  supxrss  12034  infxrss  12040  iccsupr  12137  hashf1lem2  13097  trclun  13603  fsum2d  14344  fsumabs  14374  fsumrlim  14384  fsumo1  14385  fprod2d  14550  rpnnen2lem4  14785  rpnnen2lem7  14788  ramub2  15556  ressinbas  15763  ressress  15765  submre  16088  mrcss  16099  mreacs  16142  drsdirfi  16761  clatglbss  16950  ipopos  16983  cntz2ss  17588  ablfac1eulem  18294  subrgint  18625  tgval  20570  mretopd  20706  ssnei  20724  opnneiss  20732  restdis  20792  restcls  20795  restntr  20796  tgcnp  20867  fbssfi  21451  fgss2  21488  fgcl  21492  supfil  21509  alexsubALTlem3  21663  alexsubALTlem4  21664  cnextcn  21681  ustex3sym  21831  trust  21843  restutop  21851  utop2nei  21864  cfiluweak  21909  blssexps  22041  blssex  22042  mopni3  22109  metss  22123  metcnp3  22155  metust  22173  cfilucfil  22174  psmetutop  22182  tgioo  22407  xrsmopn  22423  fsumcn  22481  cncfmptid  22523  iscmet3lem2  22898  caussi  22903  ovolsslem  23059  ovolsscl  23061  ovolssnul  23062  opnmblALT  23177  itgfsum  23399  limcresi  23455  dvmptfsum  23542  plyss  23759  chsupunss  27587  shsupunss  27589  spanss  27591  shslubi  27628  shlub  27657  mdsl1i  28564  mdsl2i  28565  cvmdi  28567  mdslmd1lem1  28568  mdslmd1lem2  28569  mdslmd2i  28573  mdslmd4i  28576  atomli  28625  atcvatlem  28628  chirredlem2  28634  chirredi  28637  mdsymlem5  28650  xrge0infss  28915  tpr2rico  29286  sigainb  29526  dya2icoseg2  29667  omssubadd  29689  eulerpartlemn  29770  ballotlem2  29877  cvmlift2lem12  30550  opnbnd  31490  fneint  31513  dissneqlem  32363  fin2so  32566  matunitlindflem1  32575  mblfinlem4  32619  ismblfin  32620  filbcmb  32705  heiborlem10  32789  igenmin  33033  lssatle  33320  paddss1  34121  paddss2  34122  paddss12  34123  paddssw2  34148  pclssN  34198  pclfinN  34204  polsubN  34211  2polvalN  34218  2polssN  34219  3polN  34220  2pmaplubN  34230  pnonsingN  34237  polsubclN  34256  dihord6apre  35563  dochsscl  35675  mapdordlem2  35944  isnacs3  36291  itgoss  36752  sspwimp  38176  sspwimpVD  38177  nsstr  38301  islptre  38686  nbuhgr  40565  gsumlsscl  41958  lincellss  42009  ellcoellss  42018
  Copyright terms: Public domain W3C validator