Theorem sstr 3941

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

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

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

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

This theorem is referenced by:  sstrd  3943  sylan9ss  3946  ssdifss  4088  uneqin  4237  intss2  5054  ssrnres  6122  relrelss  6216  fcof  6670  fssres  6685  ssimaex  6902  dff3  7028  tpostpos2  8172  smores  8267  om00  8485  omeulem2  8493  cofonr  8584  naddunif  8603  pmss12g  8788  unblem1  9171  unblem2  9172  unblem3  9173  unblem4  9174  isfinite2  9177  cantnfval2  9554  cantnfle  9556  rankxplim3  9766  alephinit  9978  dfac12lem2  10028  ackbij1lem11  10112  cfeq0  10139  cfsuc  10140  cff1  10141  cflim2  10146  cfss  10148  cfslb2n  10151  cofsmo  10152  cfsmolem  10153  fin23lem34  10229  fin1a2lem13  10295  axdc3lem2  10334  axdclem  10402  pwcfsdom  10466  wunfi  10604  tskxpss  10655  tskcard  10664  suprzcl  12545  uzwo  12801  uzwo2  12802  infssuzle  12821  infssuzcl  12822  supxrbnd  13219  supxrgtmnf  13220  supxrre1  13221  supxrre2  13222  supxrss  13223  infxrss  13231  iccsupr  13334  hashf1lem2  14355  trclun  14913  fsum2d  15670  fsumabs  15700  fsumrlim  15710  fsumo1  15711  fprod2d  15880  rpnnen2lem4  16118  rpnnen2lem7  16121  ramub2  16918  ressinbas  17148  ressress  17150  submre  17499  mrcss  17514  mreacs  17556  drsdirfi  18203  clatglbss  18417  ipopos  18434  chnrdss  18515  cntz2ss  19240  pgrpsubgsymg  19314  ablfac1eulem  19979  subrngint  20468  subrgint  20503  tgval  22863  mretopd  23000  ssnei  23018  opnneiss  23026  restdis  23086  restcls  23089  restntr  23090  tgcnp  23161  fbssfi  23745  fgss2  23782  fgcl  23786  supfil  23803  alexsubALTlem3  23957  alexsubALTlem4  23958  cnextcn  23975  ustex3sym  24126  trust  24137  restutop  24145  utop2nei  24158  cfiluweak  24202  blssexps  24334  blssex  24335  mopni3  24402  metss  24416  metcnp3  24448  metust  24466  cfilucfil  24467  psmetutop  24475  tgioo  24704  xrsmopn  24721  fsumcn  24781  cncfmptid  24826  iscmet3lem2  25212  caussi  25217  ovolsslem  25405  ovolsscl  25407  ovolssnul  25408  opnmblALT  25524  itgfsum  25748  limcresi  25806  dvmptfsum  25899  plyss  26124  madebdayim  27826  cofcutrtime  27864  n0sfincut  28275  nbuhgr  29314  chsupunss  31314  shsupunss  31316  spanss  31318  shslubi  31355  shlub  31384  mdsl1i  32291  mdsl2i  32292  cvmdi  32294  mdslmd1lem1  32295  mdslmd1lem2  32296  mdslmd2i  32300  mdslmd4i  32303  atomli  32352  atcvatlem  32355  chirredlem2  32361  chirredi  32364  mdsymlem5  32377  xrge0infss  32733  tpr2rico  33915  sigainb  34139  dya2icoseg2  34281  omssubadd  34303  eulerpartlemn  34384  ballotlem2  34492  nummin  35093  cvmlift2lem12  35326  opnbnd  36338  fneint  36361  dissneqlem  37353  inunissunidif  37388  pibt2  37430  fin2so  37626  matunitlindflem1  37635  mblfinlem4  37679  ismblfin  37680  filbcmb  37759  heiborlem10  37839  igenmin  38083  lssatle  39033  paddss1  39835  paddss2  39836  paddss12  39837  paddssw2  39862  pclssN  39912  pclfinN  39918  polsubN  39925  2polvalN  39932  2polssN  39933  3polN  39934  2pmaplubN  39944  pnonsingN  39951  polsubclN  39970  dihord6apre  41274  dochsscl  41386  mapdordlem2  41655  isnacs3  42722  itgoss  43175  ofoaid1  43370  ofoaid2  43371  sspwimp  44929  sspwimpVD  44930  nsstr  45111  islptre  45638  gsumlsscl  48390  lincellss  48437  ellcoellss  48446