Theorem sstr 3967

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

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

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 3943

This theorem is referenced by:  sstrd  3969  sylan9ss  3972  ssdifss  4115  uneqin  4264  intss2  5084  ssrnres  6167  relrelss  6262  fcof  6728  fssres  6743  ssimaex  6963  dff3  7089  tpostpos2  8244  smores  8364  om00  8585  omeulem2  8593  cofonr  8684  naddunif  8703  pmss12g  8881  unblem1  9298  unblem2  9299  unblem3  9300  unblem4  9301  isfinite2  9304  cantnfval2  9681  cantnfle  9683  rankxplim3  9893  alephinit  10107  dfac12lem2  10157  ackbij1lem11  10241  cfeq0  10268  cfsuc  10269  cff1  10270  cflim2  10275  cfss  10277  cfslb2n  10280  cofsmo  10281  cfsmolem  10282  fin23lem34  10358  fin1a2lem13  10424  axdc3lem2  10463  axdclem  10531  pwcfsdom  10595  wunfi  10733  tskxpss  10784  tskcard  10793  suprzcl  12671  uzwo  12925  uzwo2  12926  infssuzle  12945  infssuzcl  12946  supxrbnd  13342  supxrgtmnf  13343  supxrre1  13344  supxrre2  13345  supxrss  13346  infxrss  13354  iccsupr  13457  hashf1lem2  14472  trclun  15031  fsum2d  15785  fsumabs  15815  fsumrlim  15825  fsumo1  15826  fprod2d  15995  rpnnen2lem4  16233  rpnnen2lem7  16236  ramub2  17032  ressinbas  17264  ressress  17266  submre  17615  mrcss  17626  mreacs  17668  drsdirfi  18315  clatglbss  18527  ipopos  18544  cntz2ss  19316  pgrpsubgsymg  19388  ablfac1eulem  20053  subrngint  20518  subrgint  20553  tgval  22891  mretopd  23028  ssnei  23046  opnneiss  23054  restdis  23114  restcls  23117  restntr  23118  tgcnp  23189  fbssfi  23773  fgss2  23810  fgcl  23814  supfil  23831  alexsubALTlem3  23985  alexsubALTlem4  23986  cnextcn  24003  ustex3sym  24154  trust  24166  restutop  24174  utop2nei  24187  cfiluweak  24231  blssexps  24363  blssex  24364  mopni3  24431  metss  24445  metcnp3  24477  metust  24495  cfilucfil  24496  psmetutop  24504  tgioo  24733  xrsmopn  24750  fsumcn  24810  cncfmptid  24855  iscmet3lem2  25242  caussi  25247  ovolsslem  25435  ovolsscl  25437  ovolssnul  25438  opnmblALT  25554  itgfsum  25778  limcresi  25836  dvmptfsum  25929  plyss  26154  madebdayim  27843  cofcutrtime  27878  nbuhgr  29268  chsupunss  31271  shsupunss  31273  spanss  31275  shslubi  31312  shlub  31341  mdsl1i  32248  mdsl2i  32249  cvmdi  32251  mdslmd1lem1  32252  mdslmd1lem2  32253  mdslmd2i  32257  mdslmd4i  32260  atomli  32309  atcvatlem  32312  chirredlem2  32318  chirredi  32321  mdsymlem5  32334  xrge0infss  32683  tpr2rico  33889  sigainb  34113  dya2icoseg2  34256  omssubadd  34278  eulerpartlemn  34359  ballotlem2  34467  nummin  35068  cvmlift2lem12  35282  opnbnd  36289  fneint  36312  dissneqlem  37304  inunissunidif  37339  pibt2  37381  fin2so  37577  matunitlindflem1  37586  mblfinlem4  37630  ismblfin  37631  filbcmb  37710  heiborlem10  37790  igenmin  38034  lssatle  38979  paddss1  39782  paddss2  39783  paddss12  39784  paddssw2  39809  pclssN  39859  pclfinN  39865  polsubN  39872  2polvalN  39879  2polssN  39880  3polN  39881  2pmaplubN  39891  pnonsingN  39898  polsubclN  39917  dihord6apre  41221  dochsscl  41333  mapdordlem2  41602  isnacs3  42680  itgoss  43134  ofoaid1  43329  ofoaid2  43330  sspwimp  44890  sspwimpVD  44891  nsstr  45067  islptre  45596  gsumlsscl  48303  lincellss  48350  ellcoellss  48359