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

Theorem sstr 3359
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 3358 . 2  |-  ( A 
C_  B  ->  ( B  C_  C  ->  A  C_  C ) )
21imp 429 1  |-  ( ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    C_ wss 3323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3330  df-ss 3337
This theorem is referenced by:  sstrd  3361  sylan9ss  3364  ssdifss  3482  uneqin  3596  ssrnres  5271  relrelss  5356  fco  5563  fssres  5573  ssimaex  5751  dff3  5851  tpostpos2  6761  smores  6805  om00  7006  omeulem2  7014  pmss12g  7231  unblem1  7556  unblem2  7557  unblem3  7558  unblem4  7559  isfinite2  7562  cantnfval2  7869  cantnfle  7871  cantnfval2OLD  7899  cantnfleOLD  7901  rankxplim3  8080  alephinit  8257  dfac12lem2  8305  ackbij1lem11  8391  cfeq0  8417  cfsuc  8418  cff1  8419  cflim2  8424  cfss  8426  cfslb2n  8429  cofsmo  8430  cfsmolem  8431  fin23lem34  8507  fin1a2lem13  8573  axdc3lem2  8612  axdclem  8680  pwcfsdom  8739  wunfi  8880  tskxpss  8931  tskcard  8940  suprzcl  10713  uzwo  10909  uzwoOLD  10910  uzwo2  10911  infmssuzle  10929  infmssuzcl  10930  supxrbnd  11283  supxrgtmnf  11284  supxrre1  11285  supxrre2  11286  supxrss  11287  iccsupr  11374  hashf1lem2  12201  fsum2d  13230  fsumabs  13256  fsumrlim  13266  fsumo1  13267  rpnnen2lem4  13492  rpnnen2lem7  13495  ramub2  14067  ressinbas  14226  ressress  14227  submre  14535  mrcss  14546  mreacs  14588  drsdirfi  15100  clatglbss  15289  ipopos  15322  cntz2ss  15841  ablfac1eulem  16563  subrgint  16867  tgval  18540  unitg  18552  mretopd  18676  ssnei  18694  opnneiss  18702  restdis  18762  restcls  18765  restntr  18766  tgcnp  18837  fbssfi  19390  fgss2  19427  fgcl  19431  supfil  19448  alexsubALTlem3  19601  alexsubALTlem4  19602  cnextcn  19619  ustex3sym  19772  trust  19784  restutop  19792  utop2nei  19805  cfiluweak  19850  blssexps  19981  blssex  19982  mopni3  20049  metss  20063  metcnp3  20095  metustOLD  20122  metust  20123  cfilucfilOLD  20124  cfilucfil  20125  metutopOLD  20137  psmetutop  20138  tgioo  20353  xrsmopn  20369  fsumcn  20426  cncfmptid  20468  iscmet3lem2  20783  caussi  20788  ovolsslem  20947  ovolsscl  20949  ovolssnul  20950  opnmblALT  21063  itgfsum  21284  limcresi  21340  dvmptfsum  21427  plyss  21647  chsupunss  24715  shsupunss  24717  spanss  24719  shslubi  24756  shlub  24785  mdsl1i  25693  mdsl2i  25694  cvmdi  25696  mdslmd1lem1  25697  mdslmd1lem2  25698  mdslmd2i  25702  mdslmd4i  25705  atomli  25754  atcvatlem  25757  chirredlem2  25763  chirredi  25766  mdsymlem5  25779  xrge0infss  26021  tpr2rico  26311  sigainb  26548  dya2icoseg2  26662  eulerpartlemn  26733  ballotlem2  26840  cvmlift2lem12  27172  fprod2d  27461  fin2so  28387  mblfinlem4  28402  ismblfin  28403  opnbnd  28491  fneint  28520  filbcmb  28605  heiborlem10  28690  igenmin  28835  isnacs3  29017  itgoss  29491  gsumlsscl  30780  lincellss  30891  ellcoellss  30900  sspwimp  31583  sspwimpVD  31584  lssatle  32553  paddss1  33354  paddss2  33355  paddss12  33356  paddssw2  33381  pclssN  33431  pclfinN  33437  polsubN  33444  2polvalN  33451  2polssN  33452  3polN  33453  2pmaplubN  33463  pnonsingN  33470  polsubclN  33489  dihord6apre  34794  dochsscl  34906  mapdordlem2  35175
  Copyright terms: Public domain W3C validator