Theorem sstr 3938

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

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

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

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

This theorem is referenced by:  sstrd  3940  sylan9ss  3943  ssdifss  4087  uneqin  4236  intss2  5054  ssrnres  6125  relrelss  6220  fcof  6674  fssres  6689  ssimaex  6907  dff3  7033  tpostpos2  8177  smores  8272  om00  8490  omeulem2  8498  cofonr  8589  naddunif  8608  pmss12g  8793  unblem1  9176  unblem2  9177  unblem3  9178  unblem4  9179  isfinite2  9182  cantnfval2  9559  cantnfle  9561  rankxplim3  9774  alephinit  9986  dfac12lem2  10036  ackbij1lem11  10120  cfeq0  10147  cfsuc  10148  cff1  10149  cflim2  10154  cfss  10156  cfslb2n  10159  cofsmo  10160  cfsmolem  10161  fin23lem34  10237  fin1a2lem13  10303  axdc3lem2  10342  axdclem  10410  pwcfsdom  10474  wunfi  10612  tskxpss  10663  tskcard  10672  suprzcl  12553  uzwo  12809  uzwo2  12810  infssuzle  12829  infssuzcl  12830  supxrbnd  13227  supxrgtmnf  13228  supxrre1  13229  supxrre2  13230  supxrss  13231  infxrss  13239  iccsupr  13342  hashf1lem2  14363  trclun  14921  fsum2d  15678  fsumabs  15708  fsumrlim  15718  fsumo1  15719  fprod2d  15888  rpnnen2lem4  16126  rpnnen2lem7  16129  ramub2  16926  ressinbas  17156  ressress  17158  submre  17507  mrcss  17522  mreacs  17564  drsdirfi  18211  clatglbss  18425  ipopos  18442  chnrdss  18523  cntz2ss  19247  pgrpsubgsymg  19321  ablfac1eulem  19986  subrngint  20475  subrgint  20510  tgval  22870  mretopd  23007  ssnei  23025  opnneiss  23033  restdis  23093  restcls  23096  restntr  23097  tgcnp  23168  fbssfi  23752  fgss2  23789  fgcl  23793  supfil  23810  alexsubALTlem3  23964  alexsubALTlem4  23965  cnextcn  23982  ustex3sym  24133  trust  24144  restutop  24152  utop2nei  24165  cfiluweak  24209  blssexps  24341  blssex  24342  mopni3  24409  metss  24423  metcnp3  24455  metust  24473  cfilucfil  24474  psmetutop  24482  tgioo  24711  xrsmopn  24728  fsumcn  24788  cncfmptid  24833  iscmet3lem2  25219  caussi  25224  ovolsslem  25412  ovolsscl  25414  ovolssnul  25415  opnmblALT  25531  itgfsum  25755  limcresi  25813  dvmptfsum  25906  plyss  26131  madebdayim  27833  cofcutrtime  27871  n0sfincut  28282  nbuhgr  29321  chsupunss  31324  shsupunss  31326  spanss  31328  shslubi  31365  shlub  31394  mdsl1i  32301  mdsl2i  32302  cvmdi  32304  mdslmd1lem1  32305  mdslmd1lem2  32306  mdslmd2i  32310  mdslmd4i  32313  atomli  32362  atcvatlem  32365  chirredlem2  32371  chirredi  32374  mdsymlem5  32387  xrge0infss  32743  tpr2rico  33925  sigainb  34149  dya2icoseg2  34291  omssubadd  34313  eulerpartlemn  34394  ballotlem2  34502  fissorduni  35101  nummin  35104  cvmlift2lem12  35358  opnbnd  36369  fneint  36392  dissneqlem  37384  inunissunidif  37419  pibt2  37461  fin2so  37646  matunitlindflem1  37655  mblfinlem4  37699  ismblfin  37700  filbcmb  37779  heiborlem10  37859  igenmin  38103  lssatle  39113  paddss1  39915  paddss2  39916  paddss12  39917  paddssw2  39942  pclssN  39992  pclfinN  39998  polsubN  40005  2polvalN  40012  2polssN  40013  3polN  40014  2pmaplubN  40024  pnonsingN  40031  polsubclN  40050  dihord6apre  41354  dochsscl  41466  mapdordlem2  41735  isnacs3  42802  itgoss  43255  ofoaid1  43450  ofoaid2  43451  sspwimp  45009  sspwimpVD  45010  nsstr  45191  islptre  45718  gsumlsscl  48479  lincellss  48526  ellcoellss  48535