Theorem sstr 3935

Description: Transitivity of subclass relationship. Theorem 6 of [Suppes] p. 23. (Contributed by NM, 5-Sep-2003.)

Assertion

Ref	Expression
sstr	⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶)

Proof of Theorem sstr

Step	Hyp	Ref	Expression
1		sstr2 3934	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
2	1	imp 409	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   ∧ wa 398   ⊆ wss 3895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819

This theorem depends on definitions:  df-bi 209  df-an 399  df-ss 3912

This theorem is referenced by:  sstrd  3937  sylan9ss  3940  ssdifss  4084  uneqin  4232  intss2  5055  ssrnres  6149  relrelss  6245  fcof  6700  fssres  6715  ssimaex  6937  dff3  7066  tpostpos2  8211  smores  8307  om00  8528  omeulem2  8536  cofonr  8628  naddunif  8648  pmss12g  8836  unblem1  9221  unblem2  9222  unblem3  9223  unblem4  9224  isfinite2  9227  cantnfval2  9610  cantnfle  9612  rankxplim3  9825  alephinit  10037  dfac12lem2  10087  ackbij1lem11  10171  cfeq0  10199  cfsuc  10200  cff1  10201  cflim2  10206  cfss  10208  cfslb2n  10211  cofsmo  10212  cfsmolem  10213  fin23lem34  10289  fin1a2lem13  10355  axdc3lem2  10394  axdclem  10462  pwcfsdom  10527  wunfi  10665  tskxpss  10716  tskcard  10725  suprzcl  12639  uzwo  12898  uzwo2  12899  infssuzle  12918  infssuzcl  12919  supxrbnd  13317  supxrgtmnf  13318  supxrre1  13319  supxrre2  13320  supxrss  13321  infxrss  13329  iccsupr  13432  hashf1lem2  14455  trclun  15013  fsum2d  15770  fsumabs  15801  fsumrlim  15811  fsumo1  15812  fprod2d  15983  rpnnen2lem4  16221  rpnnen2lem7  16224  ramub2  17022  ressinbas  17253  ressress  17255  submre  17605  mrcss  17620  mreacs  17662  drsdirfi  18309  clatglbss  18523  ipopos  18540  chnrdss  18621  cntz2ss  19347  pgrpsubgsymg  19421  ablfac1eulem  20086  subrngint  20578  subrgint  20613  tgval  22984  mretopd  23121  ssnei  23139  opnneiss  23147  restdis  23207  restcls  23210  restntr  23211  tgcnp  23282  fbssfi  23866  fgss2  23903  fgcl  23907  supfil  23924  alexsubALTlem3  24078  alexsubALTlem4  24079  cnextcn  24096  ustex3sym  24247  trust  24258  restutop  24266  utop2nei  24279  cfiluweak  24323  blssexps  24455  blssex  24456  mopni3  24523  metss  24537  metcnp3  24569  metust  24587  cfilucfil  24588  psmetutop  24596  tgioo  24825  xrsmopn  24842  fsumcn  24901  cncfmptid  24944  iscmet3lem2  25323  caussi  25328  ovolsslem  25515  ovolsscl  25517  ovolssnul  25518  opnmblALT  25634  itgfsum  25858  limcresi  25916  dvmptfsum  26006  plyss  26228  madebdayim  27947  cofcutrtime  27986  n0fincut  28414  nbuhgr  29479  chsupunss  31482  shsupunss  31484  spanss  31486  shslubi  31523  shlub  31552  mdsl1i  32459  mdsl2i  32460  cvmdi  32462  mdslmd1lem1  32463  mdslmd1lem2  32464  mdslmd2i  32468  mdslmd4i  32471  atomli  32520  atcvatlem  32523  chirredlem2  32529  chirredi  32532  mdsymlem5  32545  xrge0infss  32901  tpr2rico  34153  sigainb  34377  dya2icoseg2  34519  omssubadd  34541  eulerpartlemn  34622  ballotlem2  34730  fissorduni  35331  nummin  35334  cvmlift2lem12  35602  opnbnd  36623  fneint  36646  ttcss2  36797  ssttctr  36802  dissneqlem  37772  inunissunidif  37807  pibt2  37849  fin2so  38044  matunitlindflem1  38053  mblfinlem4  38097  ismblfin  38098  filbcmb  38177  heiborlem10  38257  igenmin  38501  lssatle  39577  paddss1  40379  paddss2  40380  paddss12  40381  paddssw2  40406  pclssN  40456  pclfinN  40462  polsubN  40469  2polvalN  40476  2polssN  40477  3polN  40478  2pmaplubN  40488  pnonsingN  40495  polsubclN  40514  dihord6apre  41818  dochsscl  41930  mapdordlem2  42199  isnacs3  43229  itgoss  43678  ofoaid1  43873  ofoaid2  43874  sspwimp  45431  sspwimpVD  45432  nsstr  45611  islptre  46133  gsumlsscl  48940  lincellss  48986  ellcoellss  48995