Theorem sstr 4003

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 4001	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
2	1	imp 406	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3962

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3979

This theorem is referenced by:  sstrd  4005  sylan9ss  4008  ssdifss  4149  uneqin  4294  intss2  5112  ssrnres  6199  relrelss  6294  fcof  6759  fssres  6774  ssimaex  6993  dff3  7119  tpostpos2  8270  smores  8390  om00  8611  omeulem2  8619  cofonr  8710  naddunif  8729  pmss12g  8907  unblem1  9325  unblem2  9326  unblem3  9327  unblem4  9328  isfinite2  9331  cantnfval2  9706  cantnfle  9708  rankxplim3  9918  alephinit  10132  dfac12lem2  10182  ackbij1lem11  10266  cfeq0  10293  cfsuc  10294  cff1  10295  cflim2  10300  cfss  10302  cfslb2n  10305  cofsmo  10306  cfsmolem  10307  fin23lem34  10383  fin1a2lem13  10449  axdc3lem2  10488  axdclem  10556  pwcfsdom  10620  wunfi  10758  tskxpss  10809  tskcard  10818  suprzcl  12695  uzwo  12950  uzwo2  12951  infssuzle  12970  infssuzcl  12971  supxrbnd  13366  supxrgtmnf  13367  supxrre1  13368  supxrre2  13369  supxrss  13370  infxrss  13377  iccsupr  13478  hashf1lem2  14491  trclun  15049  fsum2d  15803  fsumabs  15833  fsumrlim  15843  fsumo1  15844  fprod2d  16013  rpnnen2lem4  16249  rpnnen2lem7  16252  ramub2  17047  ressinbas  17290  ressress  17293  submre  17649  mrcss  17660  mreacs  17702  drsdirfi  18362  clatglbss  18576  ipopos  18593  cntz2ss  19365  pgrpsubgsymg  19441  ablfac1eulem  20106  subrngint  20576  subrgint  20611  tgval  22977  mretopd  23115  ssnei  23133  opnneiss  23141  restdis  23201  restcls  23204  restntr  23205  tgcnp  23276  fbssfi  23860  fgss2  23897  fgcl  23901  supfil  23918  alexsubALTlem3  24072  alexsubALTlem4  24073  cnextcn  24090  ustex3sym  24241  trust  24253  restutop  24261  utop2nei  24274  cfiluweak  24319  blssexps  24451  blssex  24452  mopni3  24522  metss  24536  metcnp3  24568  metust  24586  cfilucfil  24587  psmetutop  24595  tgioo  24831  xrsmopn  24847  fsumcn  24907  cncfmptid  24952  iscmet3lem2  25339  caussi  25344  ovolsslem  25532  ovolsscl  25534  ovolssnul  25535  opnmblALT  25651  itgfsum  25876  limcresi  25934  dvmptfsum  26027  plyss  26252  madebdayim  27940  cofcutrtime  27975  nbuhgr  29374  chsupunss  31372  shsupunss  31374  spanss  31376  shslubi  31413  shlub  31442  mdsl1i  32349  mdsl2i  32350  cvmdi  32352  mdslmd1lem1  32353  mdslmd1lem2  32354  mdslmd2i  32358  mdslmd4i  32361  atomli  32410  atcvatlem  32413  chirredlem2  32419  chirredi  32422  mdsymlem5  32435  xrge0infss  32770  tpr2rico  33872  sigainb  34116  dya2icoseg2  34259  omssubadd  34281  eulerpartlemn  34362  ballotlem2  34469  nummin  35083  cvmlift2lem12  35298  opnbnd  36307  fneint  36330  dissneqlem  37322  inunissunidif  37357  pibt2  37399  fin2so  37593  matunitlindflem1  37602  mblfinlem4  37646  ismblfin  37647  filbcmb  37726  heiborlem10  37806  igenmin  38050  lssatle  38996  paddss1  39799  paddss2  39800  paddss12  39801  paddssw2  39826  pclssN  39876  pclfinN  39882  polsubN  39889  2polvalN  39896  2polssN  39897  3polN  39898  2pmaplubN  39908  pnonsingN  39915  polsubclN  39934  dihord6apre  41238  dochsscl  41350  mapdordlem2  41619  isnacs3  42697  itgoss  43151  ofoaid1  43347  ofoaid2  43348  sspwimp  44915  sspwimpVD  44916  nsstr  45034  islptre  45574  gsumlsscl  48224  lincellss  48271  ellcoellss  48280