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

Theorem sstr 3148
Description: Transitivity of subclasses. Theorem 6 of [Suppes] p. 23. (Contributed by NM, 5-Sep-2003.)
Assertion
Ref Expression
sstr  |-  ( ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )

Proof of Theorem sstr
StepHypRef Expression
1 sstr2 3147 . 2  |-  ( A 
C_  B  ->  ( B  C_  C  ->  A  C_  C ) )
21imp 420 1  |-  ( ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    C_ wss 3113
This theorem is referenced by:  sstrd  3150  sylan9ss  3153  ssdifss  3268  uneqin  3381  ssrnres  5090  relrelss  5169  fco  5322  fssres  5332  ssimaex  5504  dff3  5593  tpostpos2  6175  smores  6323  om00  6527  omeulem2  6535  pmss12g  6748  unblem1  7063  unblem2  7064  unblem3  7065  unblem4  7066  isfinite2  7069  cantnfval2  7324  cantnfle  7326  rankxplim3  7505  alephinit  7676  dfac12lem2  7724  ackbij1lem11  7810  cfeq0  7836  cfsuc  7837  cff1  7838  cflim2  7843  cfss  7845  cfslb2n  7848  cofsmo  7849  cfsmolem  7850  fin23lem34  7926  fin1a2lem13  7992  axdc3lem2  8031  axdclem  8100  pwcfsdom  8159  wunfi  8297  tskxpss  8348  tskcard  8357  suprzcl  10044  uzwo  10234  uzwoOLD  10235  uzwo2  10236  infmssuzle  10253  infmssuzcl  10254  supxrbnd  10599  supxrgtmnf  10600  supxrre1  10601  supxrre2  10602  supxrss  10603  iccsupr  10688  hashf1lem2  11345  fsum2d  12185  fsumabs  12210  fsumrlim  12220  fsumo1  12221  rpnnen2lem4  12444  rpnnen2lem7  12447  ramub2  13009  ressinbas  13152  ressress  13153  submre  13455  mrcss  13466  mreacs  13508  drsdirfi  14020  clatglbss  14179  ipopos  14211  cntz2ss  14756  ablfac1eulem  15255  subrgint  15515  tgval  16641  unitg  16653  mretopd  16777  ssnei  16795  opnneiss  16803  restdis  16857  restcls  16859  restntr  16860  tgcnp  16931  fbssfi  17480  fgss2  17517  fgcl  17521  supfil  17538  alexsubALTlem3  17691  alexsubALTlem4  17692  blssex  17921  mopni3  17988  metss  18002  metcnp3  18034  tgioo  18250  xrsmopn  18266  fsumcn  18322  cncfmptid  18364  iscmet3lem2  18666  caussi  18671  ovolsslem  18791  ovolsscl  18793  ovolssnul  18794  opnmblALT  18906  itgfsum  19129  limcresi  19183  dvmptfsum  19270  plyss  19529  chsupunss  21869  shsupunss  21871  spanss  21873  shslubi  21910  shlub  21939  mdsl1i  22847  mdsl2i  22848  cvmdi  22850  mdslmd1lem1  22851  mdslmd1lem2  22852  mdslmd2i  22856  mdslmd4i  22859  atomli  22908  atcvatlem  22911  chirredlem2  22917  chirredi  22920  mdsymlem5  22933  ballotlem2  22994  cvmlift2lem12  23203  inttrp  24460  int2pre  24590  fisub  24907  cmptdst  24921  limptlimpr2lem2  24928  islimrs4  24935  hdrmp  25059  dmrngcmp  25104  prismorcsetlemc  25270  lemindclsbu  25348  iscol3  25447  opnbnd  25596  fneint  25630  filbcmb  25785  lpss2  25821  heiborlem10  25897  igenmin  26042  isnacs3  26138  itgoss  26721  stoweidlem34  27104  stoweidlem57  27127  stoweidlem59  27129  sspwimp  27728  sspwimpVD  27729  lssatle  28356  paddss1  29157  paddss2  29158  paddss12  29159  paddssw2  29184  pclssN  29234  pclfinN  29240  polsubN  29247  2polvalN  29254  2polssN  29255  3polN  29256  2pmaplubN  29266  pnonsingN  29273  polsubclN  29292  dihord6apre  30597  dochsscl  30709  mapdordlem2  30978
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-in 3120  df-ss 3127
  Copyright terms: Public domain W3C validator