Theorem sstr 3955

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

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

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

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

This theorem is referenced by:  sstrd  3957  sylan9ss  3960  ssdifss  4103  uneqin  4252  intss2  5072  ssrnres  6151  relrelss  6246  fcof  6711  fssres  6726  ssimaex  6946  dff3  7072  tpostpos2  8226  smores  8321  om00  8539  omeulem2  8547  cofonr  8638  naddunif  8657  pmss12g  8842  unblem1  9239  unblem2  9240  unblem3  9241  unblem4  9242  isfinite2  9245  cantnfval2  9622  cantnfle  9624  rankxplim3  9834  alephinit  10048  dfac12lem2  10098  ackbij1lem11  10182  cfeq0  10209  cfsuc  10210  cff1  10211  cflim2  10216  cfss  10218  cfslb2n  10221  cofsmo  10222  cfsmolem  10223  fin23lem34  10299  fin1a2lem13  10365  axdc3lem2  10404  axdclem  10472  pwcfsdom  10536  wunfi  10674  tskxpss  10725  tskcard  10734  suprzcl  12614  uzwo  12870  uzwo2  12871  infssuzle  12890  infssuzcl  12891  supxrbnd  13288  supxrgtmnf  13289  supxrre1  13290  supxrre2  13291  supxrss  13292  infxrss  13300  iccsupr  13403  hashf1lem2  14421  trclun  14980  fsum2d  15737  fsumabs  15767  fsumrlim  15777  fsumo1  15778  fprod2d  15947  rpnnen2lem4  16185  rpnnen2lem7  16188  ramub2  16985  ressinbas  17215  ressress  17217  submre  17566  mrcss  17577  mreacs  17619  drsdirfi  18266  clatglbss  18478  ipopos  18495  cntz2ss  19267  pgrpsubgsymg  19339  ablfac1eulem  20004  subrngint  20469  subrgint  20504  tgval  22842  mretopd  22979  ssnei  22997  opnneiss  23005  restdis  23065  restcls  23068  restntr  23069  tgcnp  23140  fbssfi  23724  fgss2  23761  fgcl  23765  supfil  23782  alexsubALTlem3  23936  alexsubALTlem4  23937  cnextcn  23954  ustex3sym  24105  trust  24117  restutop  24125  utop2nei  24138  cfiluweak  24182  blssexps  24314  blssex  24315  mopni3  24382  metss  24396  metcnp3  24428  metust  24446  cfilucfil  24447  psmetutop  24455  tgioo  24684  xrsmopn  24701  fsumcn  24761  cncfmptid  24806  iscmet3lem2  25192  caussi  25197  ovolsslem  25385  ovolsscl  25387  ovolssnul  25388  opnmblALT  25504  itgfsum  25728  limcresi  25786  dvmptfsum  25879  plyss  26104  madebdayim  27799  cofcutrtime  27835  n0sfincut  28246  nbuhgr  29270  chsupunss  31273  shsupunss  31275  spanss  31277  shslubi  31314  shlub  31343  mdsl1i  32250  mdsl2i  32251  cvmdi  32253  mdslmd1lem1  32254  mdslmd1lem2  32255  mdslmd2i  32259  mdslmd4i  32262  atomli  32311  atcvatlem  32314  chirredlem2  32320  chirredi  32323  mdsymlem5  32336  xrge0infss  32683  tpr2rico  33902  sigainb  34126  dya2icoseg2  34269  omssubadd  34291  eulerpartlemn  34372  ballotlem2  34480  nummin  35081  cvmlift2lem12  35301  opnbnd  36313  fneint  36336  dissneqlem  37328  inunissunidif  37363  pibt2  37405  fin2so  37601  matunitlindflem1  37610  mblfinlem4  37654  ismblfin  37655  filbcmb  37734  heiborlem10  37814  igenmin  38058  lssatle  39008  paddss1  39811  paddss2  39812  paddss12  39813  paddssw2  39838  pclssN  39888  pclfinN  39894  polsubN  39901  2polvalN  39908  2polssN  39909  3polN  39910  2pmaplubN  39920  pnonsingN  39927  polsubclN  39946  dihord6apre  41250  dochsscl  41362  mapdordlem2  41631  isnacs3  42698  itgoss  43152  ofoaid1  43347  ofoaid2  43348  sspwimp  44907  sspwimpVD  44908  nsstr  45089  islptre  45617  gsumlsscl  48368  lincellss  48415  ellcoellss  48424