Theorem sstr 3943

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

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

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

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

This theorem is referenced by:  sstrd  3945  sylan9ss  3948  ssdifss  4093  uneqin  4242  intss2  5064  ssrnres  6137  relrelss  6232  fcof  6686  fssres  6701  ssimaex  6920  dff3  7047  tpostpos2  8191  smores  8286  om00  8504  omeulem2  8512  cofonr  8604  naddunif  8623  pmss12g  8811  unblem1  9196  unblem2  9197  unblem3  9198  unblem4  9199  isfinite2  9202  cantnfval2  9582  cantnfle  9584  rankxplim3  9797  alephinit  10009  dfac12lem2  10059  ackbij1lem11  10143  cfeq0  10170  cfsuc  10171  cff1  10172  cflim2  10177  cfss  10179  cfslb2n  10182  cofsmo  10183  cfsmolem  10184  fin23lem34  10260  fin1a2lem13  10326  axdc3lem2  10365  axdclem  10433  pwcfsdom  10498  wunfi  10636  tskxpss  10687  tskcard  10696  suprzcl  12576  uzwo  12828  uzwo2  12829  infssuzle  12848  infssuzcl  12849  supxrbnd  13247  supxrgtmnf  13248  supxrre1  13249  supxrre2  13250  supxrss  13251  infxrss  13259  iccsupr  13362  hashf1lem2  14383  trclun  14941  fsum2d  15698  fsumabs  15728  fsumrlim  15738  fsumo1  15739  fprod2d  15908  rpnnen2lem4  16146  rpnnen2lem7  16149  ramub2  16946  ressinbas  17176  ressress  17178  submre  17528  mrcss  17543  mreacs  17585  drsdirfi  18232  clatglbss  18446  ipopos  18463  chnrdss  18544  cntz2ss  19268  pgrpsubgsymg  19342  ablfac1eulem  20007  subrngint  20497  subrgint  20532  tgval  22903  mretopd  23040  ssnei  23058  opnneiss  23066  restdis  23126  restcls  23129  restntr  23130  tgcnp  23201  fbssfi  23785  fgss2  23822  fgcl  23826  supfil  23843  alexsubALTlem3  23997  alexsubALTlem4  23998  cnextcn  24015  ustex3sym  24166  trust  24177  restutop  24185  utop2nei  24198  cfiluweak  24242  blssexps  24374  blssex  24375  mopni3  24442  metss  24456  metcnp3  24488  metust  24506  cfilucfil  24507  psmetutop  24515  tgioo  24744  xrsmopn  24761  fsumcn  24821  cncfmptid  24866  iscmet3lem2  25252  caussi  25257  ovolsslem  25445  ovolsscl  25447  ovolssnul  25448  opnmblALT  25564  itgfsum  25788  limcresi  25846  dvmptfsum  25939  plyss  26164  madebdayim  27870  cofcutrtime  27909  n0sfincut  28335  nbuhgr  29399  chsupunss  31402  shsupunss  31404  spanss  31406  shslubi  31443  shlub  31472  mdsl1i  32379  mdsl2i  32380  cvmdi  32382  mdslmd1lem1  32383  mdslmd1lem2  32384  mdslmd2i  32388  mdslmd4i  32391  atomli  32440  atcvatlem  32443  chirredlem2  32449  chirredi  32452  mdsymlem5  32465  xrge0infss  32821  tpr2rico  34050  sigainb  34274  dya2icoseg2  34416  omssubadd  34438  eulerpartlemn  34519  ballotlem2  34627  fissorduni  35227  nummin  35230  cvmlift2lem12  35489  opnbnd  36500  fneint  36523  dissneqlem  37516  inunissunidif  37551  pibt2  37593  fin2so  37779  matunitlindflem1  37788  mblfinlem4  37832  ismblfin  37833  filbcmb  37912  heiborlem10  37992  igenmin  38236  lssatle  39312  paddss1  40114  paddss2  40115  paddss12  40116  paddssw2  40141  pclssN  40191  pclfinN  40197  polsubN  40204  2polvalN  40211  2polssN  40212  3polN  40213  2pmaplubN  40223  pnonsingN  40230  polsubclN  40249  dihord6apre  41553  dochsscl  41665  mapdordlem2  41934  isnacs3  42988  itgoss  43441  ofoaid1  43636  ofoaid2  43637  sspwimp  45194  sspwimpVD  45195  nsstr  45375  islptre  45901  gsumlsscl  48662  lincellss  48708  ellcoellss  48717