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

Theorem sstr 3471
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 3470 . 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 3435
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3442  df-ss 3449
This theorem is referenced by:  sstrd  3473  sylan9ss  3476  ssdifss  3594  uneqin  3708  ssrnres  5383  relrelss  5468  fco  5675  fssres  5685  ssimaex  5864  dff3  5964  tpostpos2  6875  smores  6922  om00  7123  omeulem2  7131  pmss12g  7348  unblem1  7674  unblem2  7675  unblem3  7676  unblem4  7677  isfinite2  7680  cantnfval2  7987  cantnfle  7989  cantnfval2OLD  8017  cantnfleOLD  8019  rankxplim3  8198  alephinit  8375  dfac12lem2  8423  ackbij1lem11  8509  cfeq0  8535  cfsuc  8536  cff1  8537  cflim2  8542  cfss  8544  cfslb2n  8547  cofsmo  8548  cfsmolem  8549  fin23lem34  8625  fin1a2lem13  8691  axdc3lem2  8730  axdclem  8798  pwcfsdom  8857  wunfi  8998  tskxpss  9049  tskcard  9058  suprzcl  10831  uzwo  11027  uzwoOLD  11028  uzwo2  11029  infmssuzle  11047  infmssuzcl  11048  supxrbnd  11401  supxrgtmnf  11402  supxrre1  11403  supxrre2  11404  supxrss  11405  iccsupr  11498  hashf1lem2  12326  fsum2d  13355  fsumabs  13381  fsumrlim  13391  fsumo1  13392  rpnnen2lem4  13617  rpnnen2lem7  13620  ramub2  14192  ressinbas  14352  ressress  14353  submre  14661  mrcss  14672  mreacs  14714  drsdirfi  15226  clatglbss  15415  ipopos  15448  cntz2ss  15968  ablfac1eulem  16694  subrgint  17009  tgval  18691  unitg  18703  mretopd  18827  ssnei  18845  opnneiss  18853  restdis  18913  restcls  18916  restntr  18917  tgcnp  18988  fbssfi  19541  fgss2  19578  fgcl  19582  supfil  19599  alexsubALTlem3  19752  alexsubALTlem4  19753  cnextcn  19770  ustex3sym  19923  trust  19935  restutop  19943  utop2nei  19956  cfiluweak  20001  blssexps  20132  blssex  20133  mopni3  20200  metss  20214  metcnp3  20246  metustOLD  20273  metust  20274  cfilucfilOLD  20275  cfilucfil  20276  metutopOLD  20288  psmetutop  20289  tgioo  20504  xrsmopn  20520  fsumcn  20577  cncfmptid  20619  iscmet3lem2  20934  caussi  20939  ovolsslem  21098  ovolsscl  21100  ovolssnul  21101  opnmblALT  21215  itgfsum  21436  limcresi  21492  dvmptfsum  21579  plyss  21799  chsupunss  24898  shsupunss  24900  spanss  24902  shslubi  24939  shlub  24968  mdsl1i  25876  mdsl2i  25877  cvmdi  25879  mdslmd1lem1  25880  mdslmd1lem2  25881  mdslmd2i  25885  mdslmd4i  25888  atomli  25937  atcvatlem  25940  chirredlem2  25946  chirredi  25949  mdsymlem5  25962  xrge0infss  26203  tpr2rico  26486  sigainb  26723  dya2icoseg2  26836  eulerpartlemn  26907  ballotlem2  27014  cvmlift2lem12  27346  fprod2d  27635  fin2so  28563  mblfinlem4  28578  ismblfin  28579  opnbnd  28667  fneint  28696  filbcmb  28781  heiborlem10  28866  igenmin  29011  isnacs3  29193  itgoss  29667  gsumlsscl  30968  lincellss  31078  ellcoellss  31087  sspwimp  31971  sspwimpVD  31972  lssatle  32983  paddss1  33784  paddss2  33785  paddss12  33786  paddssw2  33811  pclssN  33861  pclfinN  33867  polsubN  33874  2polvalN  33881  2polssN  33882  3polN  33883  2pmaplubN  33893  pnonsingN  33900  polsubclN  33919  dihord6apre  35224  dochsscl  35336  mapdordlem2  35605
  Copyright terms: Public domain W3C validator