Theorem sstr 3929

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

Syntax hints:   → wi 4   ∧ wa 396   ⊆ wss 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  sstrd  3931  sylan9ss  3934  ssdifss  4070  uneqin  4212  intss2  5037  ssrnres  6081  relrelss  6176  fcof  6623  fcoOLD  6625  fssres  6640  ssimaex  6853  dff3  6976  tpostpos2  8063  smores  8183  om00  8406  omeulem2  8414  pmss12g  8657  unblem1  9066  unblem2  9067  unblem3  9068  unblem4  9069  isfinite2  9072  cantnfval2  9427  cantnfle  9429  rankxplim3  9639  alephinit  9851  dfac12lem2  9900  ackbij1lem11  9986  cfeq0  10012  cfsuc  10013  cff1  10014  cflim2  10019  cfss  10021  cfslb2n  10024  cofsmo  10025  cfsmolem  10026  fin23lem34  10102  fin1a2lem13  10168  axdc3lem2  10207  axdclem  10275  pwcfsdom  10339  wunfi  10477  tskxpss  10528  tskcard  10537  suprzcl  12400  uzwo  12651  uzwo2  12652  infssuzle  12671  infssuzcl  12672  supxrbnd  13062  supxrgtmnf  13063  supxrre1  13064  supxrre2  13065  supxrss  13066  infxrss  13073  iccsupr  13174  hashf1lem2  14170  trclun  14725  fsum2d  15483  fsumabs  15513  fsumrlim  15523  fsumo1  15524  fprod2d  15691  rpnnen2lem4  15926  rpnnen2lem7  15929  ramub2  16715  ressinbas  16955  ressress  16958  submre  17314  mrcss  17325  mreacs  17367  drsdirfi  18023  clatglbss  18237  ipopos  18254  cntz2ss  18939  pgrpsubgsymg  19017  ablfac1eulem  19675  subrgint  20046  tgval  22105  mretopd  22243  ssnei  22261  opnneiss  22269  restdis  22329  restcls  22332  restntr  22333  tgcnp  22404  fbssfi  22988  fgss2  23025  fgcl  23029  supfil  23046  alexsubALTlem3  23200  alexsubALTlem4  23201  cnextcn  23218  ustex3sym  23369  trust  23381  restutop  23389  utop2nei  23402  cfiluweak  23447  blssexps  23579  blssex  23580  mopni3  23650  metss  23664  metcnp3  23696  metust  23714  cfilucfil  23715  psmetutop  23723  tgioo  23959  xrsmopn  23975  fsumcn  24033  cncfmptid  24076  iscmet3lem2  24456  caussi  24461  ovolsslem  24648  ovolsscl  24650  ovolssnul  24651  opnmblALT  24767  itgfsum  24991  limcresi  25049  dvmptfsum  25139  plyss  25360  nbuhgr  27710  chsupunss  29706  shsupunss  29708  spanss  29710  shslubi  29747  shlub  29776  mdsl1i  30683  mdsl2i  30684  cvmdi  30686  mdslmd1lem1  30687  mdslmd1lem2  30688  mdslmd2i  30692  mdslmd4i  30695  atomli  30744  atcvatlem  30747  chirredlem2  30753  chirredi  30756  mdsymlem5  30769  xrge0infss  31083  tpr2rico  31862  sigainb  32104  dya2icoseg2  32245  omssubadd  32267  eulerpartlemn  32348  ballotlem2  32455  nummin  33063  cvmlift2lem12  33276  madebdayim  34070  cofcutrtime  34093  opnbnd  34514  fneint  34537  dissneqlem  35511  inunissunidif  35546  pibt2  35588  fin2so  35764  matunitlindflem1  35773  mblfinlem4  35817  ismblfin  35818  filbcmb  35898  heiborlem10  35978  igenmin  36222  lssatle  37029  paddss1  37831  paddss2  37832  paddss12  37833  paddssw2  37858  pclssN  37908  pclfinN  37914  polsubN  37921  2polvalN  37928  2polssN  37929  3polN  37930  2pmaplubN  37940  pnonsingN  37947  polsubclN  37966  dihord6apre  39270  dochsscl  39382  mapdordlem2  39651  isnacs3  40532  itgoss  40988  sspwimp  42538  sspwimpVD  42539  nsstr  42645  islptre  43160  gsumlsscl  45719  lincellss  45767  ellcoellss  45776