Theorem sstr 3946

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

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

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 3922

This theorem is referenced by:  sstrd  3948  sylan9ss  3951  ssdifss  4093  uneqin  4242  intss2  5060  ssrnres  6131  relrelss  6225  fcof  6679  fssres  6694  ssimaex  6912  dff3  7038  tpostpos2  8187  smores  8282  om00  8500  omeulem2  8508  cofonr  8599  naddunif  8618  pmss12g  8803  unblem1  9197  unblem2  9198  unblem3  9199  unblem4  9200  isfinite2  9203  cantnfval2  9584  cantnfle  9586  rankxplim3  9796  alephinit  10008  dfac12lem2  10058  ackbij1lem11  10142  cfeq0  10169  cfsuc  10170  cff1  10171  cflim2  10176  cfss  10178  cfslb2n  10181  cofsmo  10182  cfsmolem  10183  fin23lem34  10259  fin1a2lem13  10325  axdc3lem2  10364  axdclem  10432  pwcfsdom  10496  wunfi  10634  tskxpss  10685  tskcard  10694  suprzcl  12574  uzwo  12830  uzwo2  12831  infssuzle  12850  infssuzcl  12851  supxrbnd  13248  supxrgtmnf  13249  supxrre1  13250  supxrre2  13251  supxrss  13252  infxrss  13260  iccsupr  13363  hashf1lem2  14381  trclun  14939  fsum2d  15696  fsumabs  15726  fsumrlim  15736  fsumo1  15737  fprod2d  15906  rpnnen2lem4  16144  rpnnen2lem7  16147  ramub2  16944  ressinbas  17174  ressress  17176  submre  17525  mrcss  17540  mreacs  17582  drsdirfi  18229  clatglbss  18443  ipopos  18460  cntz2ss  19232  pgrpsubgsymg  19306  ablfac1eulem  19971  subrngint  20463  subrgint  20498  tgval  22858  mretopd  22995  ssnei  23013  opnneiss  23021  restdis  23081  restcls  23084  restntr  23085  tgcnp  23156  fbssfi  23740  fgss2  23777  fgcl  23781  supfil  23798  alexsubALTlem3  23952  alexsubALTlem4  23953  cnextcn  23970  ustex3sym  24121  trust  24133  restutop  24141  utop2nei  24154  cfiluweak  24198  blssexps  24330  blssex  24331  mopni3  24398  metss  24412  metcnp3  24444  metust  24462  cfilucfil  24463  psmetutop  24471  tgioo  24700  xrsmopn  24717  fsumcn  24777  cncfmptid  24822  iscmet3lem2  25208  caussi  25213  ovolsslem  25401  ovolsscl  25403  ovolssnul  25404  opnmblALT  25520  itgfsum  25744  limcresi  25802  dvmptfsum  25895  plyss  26120  madebdayim  27820  cofcutrtime  27858  n0sfincut  28269  nbuhgr  29306  chsupunss  31306  shsupunss  31308  spanss  31310  shslubi  31347  shlub  31376  mdsl1i  32283  mdsl2i  32284  cvmdi  32286  mdslmd1lem1  32287  mdslmd1lem2  32288  mdslmd2i  32292  mdslmd4i  32295  atomli  32344  atcvatlem  32347  chirredlem2  32353  chirredi  32356  mdsymlem5  32369  xrge0infss  32716  tpr2rico  33878  sigainb  34102  dya2icoseg2  34245  omssubadd  34267  eulerpartlemn  34348  ballotlem2  34456  nummin  35057  cvmlift2lem12  35286  opnbnd  36298  fneint  36321  dissneqlem  37313  inunissunidif  37348  pibt2  37390  fin2so  37586  matunitlindflem1  37595  mblfinlem4  37639  ismblfin  37640  filbcmb  37719  heiborlem10  37799  igenmin  38043  lssatle  38993  paddss1  39796  paddss2  39797  paddss12  39798  paddssw2  39823  pclssN  39873  pclfinN  39879  polsubN  39886  2polvalN  39893  2polssN  39894  3polN  39895  2pmaplubN  39905  pnonsingN  39912  polsubclN  39931  dihord6apre  41235  dochsscl  41347  mapdordlem2  41616  isnacs3  42683  itgoss  43136  ofoaid1  43331  ofoaid2  43332  sspwimp  44891  sspwimpVD  44892  nsstr  45073  islptre  45601  gsumlsscl  48352  lincellss  48399  ellcoellss  48408