Theorem sstr 3958

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

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

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 3934

This theorem is referenced by:  sstrd  3960  sylan9ss  3963  ssdifss  4106  uneqin  4255  intss2  5075  ssrnres  6154  relrelss  6249  fcof  6714  fssres  6729  ssimaex  6949  dff3  7075  tpostpos2  8229  smores  8324  om00  8542  omeulem2  8550  cofonr  8641  naddunif  8660  pmss12g  8845  unblem1  9246  unblem2  9247  unblem3  9248  unblem4  9249  isfinite2  9252  cantnfval2  9629  cantnfle  9631  rankxplim3  9841  alephinit  10055  dfac12lem2  10105  ackbij1lem11  10189  cfeq0  10216  cfsuc  10217  cff1  10218  cflim2  10223  cfss  10225  cfslb2n  10228  cofsmo  10229  cfsmolem  10230  fin23lem34  10306  fin1a2lem13  10372  axdc3lem2  10411  axdclem  10479  pwcfsdom  10543  wunfi  10681  tskxpss  10732  tskcard  10741  suprzcl  12621  uzwo  12877  uzwo2  12878  infssuzle  12897  infssuzcl  12898  supxrbnd  13295  supxrgtmnf  13296  supxrre1  13297  supxrre2  13298  supxrss  13299  infxrss  13307  iccsupr  13410  hashf1lem2  14428  trclun  14987  fsum2d  15744  fsumabs  15774  fsumrlim  15784  fsumo1  15785  fprod2d  15954  rpnnen2lem4  16192  rpnnen2lem7  16195  ramub2  16992  ressinbas  17222  ressress  17224  submre  17573  mrcss  17584  mreacs  17626  drsdirfi  18273  clatglbss  18485  ipopos  18502  cntz2ss  19274  pgrpsubgsymg  19346  ablfac1eulem  20011  subrngint  20476  subrgint  20511  tgval  22849  mretopd  22986  ssnei  23004  opnneiss  23012  restdis  23072  restcls  23075  restntr  23076  tgcnp  23147  fbssfi  23731  fgss2  23768  fgcl  23772  supfil  23789  alexsubALTlem3  23943  alexsubALTlem4  23944  cnextcn  23961  ustex3sym  24112  trust  24124  restutop  24132  utop2nei  24145  cfiluweak  24189  blssexps  24321  blssex  24322  mopni3  24389  metss  24403  metcnp3  24435  metust  24453  cfilucfil  24454  psmetutop  24462  tgioo  24691  xrsmopn  24708  fsumcn  24768  cncfmptid  24813  iscmet3lem2  25199  caussi  25204  ovolsslem  25392  ovolsscl  25394  ovolssnul  25395  opnmblALT  25511  itgfsum  25735  limcresi  25793  dvmptfsum  25886  plyss  26111  madebdayim  27806  cofcutrtime  27842  n0sfincut  28253  nbuhgr  29277  chsupunss  31280  shsupunss  31282  spanss  31284  shslubi  31321  shlub  31350  mdsl1i  32257  mdsl2i  32258  cvmdi  32260  mdslmd1lem1  32261  mdslmd1lem2  32262  mdslmd2i  32266  mdslmd4i  32269  atomli  32318  atcvatlem  32321  chirredlem2  32327  chirredi  32330  mdsymlem5  32343  xrge0infss  32690  tpr2rico  33909  sigainb  34133  dya2icoseg2  34276  omssubadd  34298  eulerpartlemn  34379  ballotlem2  34487  nummin  35088  cvmlift2lem12  35308  opnbnd  36320  fneint  36343  dissneqlem  37335  inunissunidif  37370  pibt2  37412  fin2so  37608  matunitlindflem1  37617  mblfinlem4  37661  ismblfin  37662  filbcmb  37741  heiborlem10  37821  igenmin  38065  lssatle  39015  paddss1  39818  paddss2  39819  paddss12  39820  paddssw2  39845  pclssN  39895  pclfinN  39901  polsubN  39908  2polvalN  39915  2polssN  39916  3polN  39917  2pmaplubN  39927  pnonsingN  39934  polsubclN  39953  dihord6apre  41257  dochsscl  41369  mapdordlem2  41638  isnacs3  42705  itgoss  43159  ofoaid1  43354  ofoaid2  43355  sspwimp  44914  sspwimpVD  44915  nsstr  45096  islptre  45624  gsumlsscl  48372  lincellss  48419  ellcoellss  48428