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

Theorem sstr 3452
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 3451 . 2  |-  ( A 
C_  B  ->  ( B  C_  C  ->  A  C_  C ) )
21imp 435 1  |-  ( ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    C_ wss 3416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-in 3423  df-ss 3430
This theorem is referenced by:  sstrd  3454  sylan9ss  3457  ssdifss  3576  uneqin  3706  ssrnres  5297  relrelss  5382  fco  5766  fssres  5776  ssimaex  5958  dff3  6063  tpostpos2  7025  smores  7102  om00  7307  omeulem2  7315  pmss12g  7529  unblem1  7854  unblem2  7855  unblem3  7856  unblem4  7857  isfinite2  7860  cantnfval2  8205  cantnfle  8207  rankxplim3  8383  alephinit  8557  dfac12lem2  8605  ackbij1lem11  8691  cfeq0  8717  cfsuc  8718  cff1  8719  cflim2  8724  cfss  8726  cfslb2n  8729  cofsmo  8730  cfsmolem  8731  fin23lem34  8807  fin1a2lem13  8873  axdc3lem2  8912  axdclem  8980  pwcfsdom  9039  wunfi  9177  tskxpss  9228  tskcard  9237  suprzcl  11049  uzwo  11256  uzwo2  11257  infssuzle  11278  infssuzcl  11279  infmssuzleOLD  11280  infmssuzclOLD  11281  supxrbnd  11648  supxrgtmnf  11649  supxrre1  11650  supxrre2  11651  supxrss  11652  infxrss  11662  infmxrssOLD  11663  iccsupr  11761  hashf1lem2  12658  trclun  13133  fsum2d  13887  fsumabs  13916  fsumrlim  13926  fsumo1  13927  fprod2d  14090  rpnnen2lem4  14325  rpnnen2lem7  14328  ramub2  15026  ressinbas  15240  ressress  15242  submre  15566  mrcss  15577  mreacs  15619  drsdirfi  16238  clatglbss  16428  ipopos  16461  cntz2ss  17041  ablfac1eulem  17760  subrgint  18085  tgval  20025  unitgOLD  20038  mretopd  20163  ssnei  20181  opnneiss  20189  restdis  20249  restcls  20252  restntr  20253  tgcnp  20324  fbssfi  20907  fgss2  20944  fgcl  20948  supfil  20965  alexsubALTlem3  21119  alexsubALTlem4  21120  cnextcn  21137  ustex3sym  21287  trust  21299  restutop  21307  utop2nei  21320  cfiluweak  21365  blssexps  21496  blssex  21497  mopni3  21564  metss  21578  metcnp3  21610  metust  21628  cfilucfil  21629  psmetutop  21637  tgioo  21869  xrsmopn  21885  fsumcn  21957  cncfmptid  21999  iscmet3lem2  22317  caussi  22322  ovolsslem  22492  ovolsscl  22494  ovolssnul  22495  opnmblALT  22617  itgfsum  22840  limcresi  22896  dvmptfsum  22983  plyss  23209  chsupunss  27053  shsupunss  27055  spanss  27057  shslubi  27094  shlub  27123  mdsl1i  28030  mdsl2i  28031  cvmdi  28033  mdslmd1lem1  28034  mdslmd1lem2  28035  mdslmd2i  28039  mdslmd4i  28042  atomli  28091  atcvatlem  28094  chirredlem2  28100  chirredi  28103  mdsymlem5  28116  xrge0infss  28392  xrge0infssOLD  28393  tpr2rico  28769  sigainb  29009  dya2icoseg2  29150  omssubadd  29178  omssubaddOLD  29182  eulerpartlemn  29264  ballotlem2  29371  cvmlift2lem12  30087  opnbnd  31031  fneint  31054  dissneqlem  31788  fin2so  31978  mblfinlem4  32026  ismblfin  32027  filbcmb  32113  heiborlem10  32198  igenmin  32343  lssatle  32627  paddss1  33428  paddss2  33429  paddss12  33430  paddssw2  33455  pclssN  33505  pclfinN  33511  polsubN  33518  2polvalN  33525  2polssN  33526  3polN  33527  2pmaplubN  33537  pnonsingN  33544  polsubclN  33563  dihord6apre  34870  dochsscl  34982  mapdordlem2  35251  isnacs3  35598  itgoss  36075  sspwimp  37356  sspwimpVD  37357  islptre  37785  nbuhgr  39557  gsumlsscl  40537  lincellss  40588  ellcoellss  40597
  Copyright terms: Public domain W3C validator