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

Theorem sstr 3478
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 3477 . 2  |-  ( A 
C_  B  ->  ( B  C_  C  ->  A  C_  C ) )
21imp 430 1  |-  ( ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    C_ wss 3442
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-in 3449  df-ss 3456
This theorem is referenced by:  sstrd  3480  sylan9ss  3483  ssdifss  3602  uneqin  3730  ssrnres  5295  relrelss  5379  fco  5756  fssres  5766  ssimaex  5946  dff3  6050  tpostpos2  7002  smores  7079  om00  7284  omeulem2  7292  pmss12g  7506  unblem1  7829  unblem2  7830  unblem3  7831  unblem4  7832  isfinite2  7835  cantnfval2  8173  cantnfle  8175  rankxplim3  8351  alephinit  8524  dfac12lem2  8572  ackbij1lem11  8658  cfeq0  8684  cfsuc  8685  cff1  8686  cflim2  8691  cfss  8693  cfslb2n  8696  cofsmo  8697  cfsmolem  8698  fin23lem34  8774  fin1a2lem13  8840  axdc3lem2  8879  axdclem  8947  pwcfsdom  9006  wunfi  9145  tskxpss  9196  tskcard  9205  suprzcl  11015  uzwo  11222  uzwo2  11223  infssuzle  11244  infssuzcl  11245  infmssuzleOLD  11246  infmssuzclOLD  11247  supxrbnd  11614  supxrgtmnf  11615  supxrre1  11616  supxrre2  11617  supxrss  11618  infxrss  11628  infmxrssOLD  11629  iccsupr  11727  hashf1lem2  12614  trclun  13057  fsum2d  13810  fsumabs  13839  fsumrlim  13849  fsumo1  13850  fprod2d  14013  rpnnen2lem4  14248  rpnnen2lem7  14251  ramub2  14925  ressinbas  15138  ressress  15140  submre  15453  mrcss  15464  mreacs  15506  drsdirfi  16125  clatglbss  16315  ipopos  16348  cntz2ss  16928  ablfac1eulem  17631  subrgint  17956  tgval  19892  unitgOLD  19905  mretopd  20030  ssnei  20048  opnneiss  20056  restdis  20116  restcls  20119  restntr  20120  tgcnp  20191  fbssfi  20774  fgss2  20811  fgcl  20815  supfil  20832  alexsubALTlem3  20986  alexsubALTlem4  20987  cnextcn  21004  ustex3sym  21154  trust  21166  restutop  21174  utop2nei  21187  cfiluweak  21232  blssexps  21363  blssex  21364  mopni3  21431  metss  21445  metcnp3  21477  metust  21495  cfilucfil  21496  psmetutop  21504  tgioo  21716  xrsmopn  21732  fsumcn  21789  cncfmptid  21831  iscmet3lem2  22146  caussi  22151  ovolsslem  22306  ovolsscl  22308  ovolssnul  22309  opnmblALT  22429  itgfsum  22652  limcresi  22708  dvmptfsum  22795  plyss  23012  chsupunss  26823  shsupunss  26825  spanss  26827  shslubi  26864  shlub  26893  mdsl1i  27800  mdsl2i  27801  cvmdi  27803  mdslmd1lem1  27804  mdslmd1lem2  27805  mdslmd2i  27809  mdslmd4i  27812  atomli  27861  atcvatlem  27864  chirredlem2  27870  chirredi  27873  mdsymlem5  27886  xrge0infss  28172  tpr2rico  28548  sigainb  28788  dya2icoseg2  28930  omssubadd  28952  eulerpartlemn  29031  ballotlem2  29138  cvmlift2lem12  29816  opnbnd  30757  fneint  30780  dissneqlem  31467  fin2so  31626  mblfinlem4  31674  ismblfin  31675  filbcmb  31761  heiborlem10  31846  igenmin  31991  lssatle  32280  paddss1  33081  paddss2  33082  paddss12  33083  paddssw2  33108  pclssN  33158  pclfinN  33164  polsubN  33171  2polvalN  33178  2polssN  33179  3polN  33180  2pmaplubN  33190  pnonsingN  33197  polsubclN  33216  dihord6apre  34523  dochsscl  34635  mapdordlem2  34904  isnacs3  35251  itgoss  35718  sspwimp  36945  sspwimpVD  36946  islptre  37261  gsumlsscl  38918  lincellss  38969  ellcoellss  38978
  Copyright terms: Public domain W3C validator