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

Theorem sstr 3425
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 3424 . 2  |-  ( A 
C_  B  ->  ( B  C_  C  ->  A  C_  C ) )
21imp 427 1  |-  ( ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    C_ wss 3389
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-in 3396  df-ss 3403
This theorem is referenced by:  sstrd  3427  sylan9ss  3430  ssdifss  3549  uneqin  3674  ssrnres  5355  relrelss  5439  fco  5649  fssres  5659  ssimaex  5839  dff3  5946  tpostpos2  6894  smores  6941  om00  7142  omeulem2  7150  pmss12g  7364  unblem1  7687  unblem2  7688  unblem3  7689  unblem4  7690  isfinite2  7693  cantnfval2  8001  cantnfle  8003  cantnfval2OLD  8031  cantnfleOLD  8033  rankxplim3  8212  alephinit  8389  dfac12lem2  8437  ackbij1lem11  8523  cfeq0  8549  cfsuc  8550  cff1  8551  cflim2  8556  cfss  8558  cfslb2n  8561  cofsmo  8562  cfsmolem  8563  fin23lem34  8639  fin1a2lem13  8705  axdc3lem2  8744  axdclem  8812  pwcfsdom  8871  wunfi  9010  tskxpss  9061  tskcard  9070  suprzcl  10859  uzwo  11064  uzwo2  11065  infmssuzle  11083  infmssuzcl  11084  supxrbnd  11441  supxrgtmnf  11442  supxrre1  11443  supxrre2  11444  supxrss  11445  iccsupr  11538  hashf1lem2  12409  trclun  12852  fsum2d  13588  fsumabs  13617  fsumrlim  13627  fsumo1  13628  fprod2d  13787  rpnnen2lem4  13953  rpnnen2lem7  13956  ramub2  14534  ressinbas  14697  ressress  14699  submre  15012  mrcss  15023  mreacs  15065  drsdirfi  15684  clatglbss  15874  ipopos  15907  cntz2ss  16487  ablfac1eulem  17236  subrgint  17564  tgval  19541  unitgOLD  19554  mretopd  19679  ssnei  19697  opnneiss  19705  restdis  19765  restcls  19768  restntr  19769  tgcnp  19840  fbssfi  20423  fgss2  20460  fgcl  20464  supfil  20481  alexsubALTlem3  20634  alexsubALTlem4  20635  cnextcn  20652  ustex3sym  20805  trust  20817  restutop  20825  utop2nei  20838  cfiluweak  20883  blssexps  21014  blssex  21015  mopni3  21082  metss  21096  metcnp3  21128  metustOLD  21155  metust  21156  cfilucfilOLD  21157  cfilucfil  21158  metutopOLD  21170  psmetutop  21171  tgioo  21386  xrsmopn  21402  fsumcn  21459  cncfmptid  21501  iscmet3lem2  21816  caussi  21821  ovolsslem  21980  ovolsscl  21982  ovolssnul  21983  opnmblALT  22097  itgfsum  22318  limcresi  22374  dvmptfsum  22461  plyss  22681  chsupunss  26379  shsupunss  26381  spanss  26383  shslubi  26420  shlub  26449  mdsl1i  27356  mdsl2i  27357  cvmdi  27359  mdslmd1lem1  27360  mdslmd1lem2  27361  mdslmd2i  27365  mdslmd4i  27368  atomli  27417  atcvatlem  27420  chirredlem2  27426  chirredi  27429  mdsymlem5  27442  xrge0infss  27730  tpr2rico  28048  sigainb  28285  dya2icoseg2  28405  omssubadd  28427  eulerpartlemn  28503  ballotlem2  28610  cvmlift2lem12  28948  fin2so  30205  mblfinlem4  30219  ismblfin  30220  opnbnd  30309  fneint  30332  filbcmb  30397  heiborlem10  30482  igenmin  30627  isnacs3  30808  itgoss  31280  infmxrss  31658  islptre  31791  gsumlsscl  33176  lincellss  33227  ellcoellss  33236  sspwimp  34065  sspwimpVD  34066  lssatle  35153  paddss1  35954  paddss2  35955  paddss12  35956  paddssw2  35981  pclssN  36031  pclfinN  36037  polsubN  36044  2polvalN  36051  2polssN  36052  3polN  36053  2pmaplubN  36063  pnonsingN  36070  polsubclN  36089  dihord6apre  37396  dochsscl  37508  mapdordlem2  37777
  Copyright terms: Public domain W3C validator