Theorem sstr 3986

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

Syntax hints:   → wi 4   ∧ wa 394   ⊆ wss 3945

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

This theorem depends on definitions:  df-bi 206  df-an 395  df-ss 3962

This theorem is referenced by:  sstrd  3988  sylan9ss  3991  ssdifss  4133  uneqin  4278  intss2  5111  ssrnres  6182  relrelss  6277  fcof  6744  fcoOLD  6746  fssres  6761  ssimaex  6980  dff3  7107  tpostpos2  8251  smores  8371  om00  8594  omeulem2  8602  cofonr  8693  naddunif  8712  pmss12g  8886  unblem1  9318  unblem2  9319  unblem3  9320  unblem4  9321  isfinite2  9324  cantnfval2  9692  cantnfle  9694  rankxplim3  9904  alephinit  10118  dfac12lem2  10167  ackbij1lem11  10253  cfeq0  10279  cfsuc  10280  cff1  10281  cflim2  10286  cfss  10288  cfslb2n  10291  cofsmo  10292  cfsmolem  10293  fin23lem34  10369  fin1a2lem13  10435  axdc3lem2  10474  axdclem  10542  pwcfsdom  10606  wunfi  10744  tskxpss  10795  tskcard  10804  suprzcl  12672  uzwo  12925  uzwo2  12926  infssuzle  12945  infssuzcl  12946  supxrbnd  13339  supxrgtmnf  13340  supxrre1  13341  supxrre2  13342  supxrss  13343  infxrss  13350  iccsupr  13451  hashf1lem2  14449  trclun  14993  fsum2d  15749  fsumabs  15779  fsumrlim  15789  fsumo1  15790  fprod2d  15957  rpnnen2lem4  16193  rpnnen2lem7  16196  ramub2  16982  ressinbas  17225  ressress  17228  submre  17584  mrcss  17595  mreacs  17637  drsdirfi  18296  clatglbss  18510  ipopos  18527  cntz2ss  19290  pgrpsubgsymg  19368  ablfac1eulem  20033  subrngint  20501  subrgint  20538  tgval  22888  mretopd  23026  ssnei  23044  opnneiss  23052  restdis  23112  restcls  23115  restntr  23116  tgcnp  23187  fbssfi  23771  fgss2  23808  fgcl  23812  supfil  23829  alexsubALTlem3  23983  alexsubALTlem4  23984  cnextcn  24001  ustex3sym  24152  trust  24164  restutop  24172  utop2nei  24185  cfiluweak  24230  blssexps  24362  blssex  24363  mopni3  24433  metss  24447  metcnp3  24479  metust  24497  cfilucfil  24498  psmetutop  24506  tgioo  24742  xrsmopn  24758  fsumcn  24818  cncfmptid  24863  iscmet3lem2  25250  caussi  25255  ovolsslem  25443  ovolsscl  25445  ovolssnul  25446  opnmblALT  25562  itgfsum  25786  limcresi  25844  dvmptfsum  25937  plyss  26163  madebdayim  27844  cofcutrtime  27877  nbuhgr  29212  chsupunss  31210  shsupunss  31212  spanss  31214  shslubi  31251  shlub  31280  mdsl1i  32187  mdsl2i  32188  cvmdi  32190  mdslmd1lem1  32191  mdslmd1lem2  32192  mdslmd2i  32196  mdslmd4i  32199  atomli  32248  atcvatlem  32251  chirredlem2  32257  chirredi  32260  mdsymlem5  32273  xrge0infss  32587  tpr2rico  33583  sigainb  33825  dya2icoseg2  33968  omssubadd  33990  eulerpartlemn  34071  ballotlem2  34178  nummin  34784  cvmlift2lem12  34994  opnbnd  35879  fneint  35902  dissneqlem  36889  inunissunidif  36924  pibt2  36966  fin2so  37150  matunitlindflem1  37159  mblfinlem4  37203  ismblfin  37204  filbcmb  37283  heiborlem10  37363  igenmin  37607  lssatle  38556  paddss1  39359  paddss2  39360  paddss12  39361  paddssw2  39386  pclssN  39436  pclfinN  39442  polsubN  39449  2polvalN  39456  2polssN  39457  3polN  39458  2pmaplubN  39468  pnonsingN  39475  polsubclN  39494  dihord6apre  40798  dochsscl  40910  mapdordlem2  41179  isnacs3  42195  itgoss  42652  ofoaid1  42852  ofoaid2  42853  sspwimp  44422  sspwimpVD  44423  nsstr  44526  islptre  45070  gsumlsscl  47559  lincellss  47606  ellcoellss  47615