Theorem sstr 3611

Description: Transitivity of subclasses. 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 3610	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
2	1	imp 445	1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   ∧ wa 384   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  sstrd  3613  sylan9ss  3616  ssdifss  3741  uneqin  3878  ssrnres  5572  relrelss  5659  fco  6058  fssres  6070  ssimaex  6263  dff3  6372  tpostpos2  7373  smores  7449  om00  7655  omeulem2  7663  pmss12g  7884  unblem1  8212  unblem2  8213  unblem3  8214  unblem4  8215  isfinite2  8218  cantnfval2  8566  cantnfle  8568  rankxplim3  8744  alephinit  8918  dfac12lem2  8966  ackbij1lem11  9052  cfeq0  9078  cfsuc  9079  cff1  9080  cflim2  9085  cfss  9087  cfslb2n  9090  cofsmo  9091  cfsmolem  9092  fin23lem34  9168  fin1a2lem13  9234  axdc3lem2  9273  axdclem  9341  pwcfsdom  9405  wunfi  9543  tskxpss  9594  tskcard  9603  suprzcl  11457  uzwo  11751  uzwo2  11752  infssuzle  11771  infssuzcl  11772  supxrbnd  12158  supxrgtmnf  12159  supxrre1  12160  supxrre2  12161  supxrss  12162  infxrss  12169  iccsupr  12266  hashf1lem2  13240  trclun  13755  fsum2d  14502  fsumabs  14533  fsumrlim  14543  fsumo1  14544  fprod2d  14711  rpnnen2lem4  14946  rpnnen2lem7  14949  ramub2  15718  ressinbas  15936  ressress  15938  submre  16265  mrcss  16276  mreacs  16319  drsdirfi  16938  clatglbss  17127  ipopos  17160  cntz2ss  17765  ablfac1eulem  18471  subrgint  18802  tgval  20759  mretopd  20896  ssnei  20914  opnneiss  20922  restdis  20982  restcls  20985  restntr  20986  tgcnp  21057  fbssfi  21641  fgss2  21678  fgcl  21682  supfil  21699  alexsubALTlem3  21853  alexsubALTlem4  21854  cnextcn  21871  ustex3sym  22021  trust  22033  restutop  22041  utop2nei  22054  cfiluweak  22099  blssexps  22231  blssex  22232  mopni3  22299  metss  22313  metcnp3  22345  metust  22363  cfilucfil  22364  psmetutop  22372  tgioo  22599  xrsmopn  22615  fsumcn  22673  cncfmptid  22715  iscmet3lem2  23090  caussi  23095  ovolsslem  23252  ovolsscl  23254  ovolssnul  23255  opnmblALT  23371  itgfsum  23593  limcresi  23649  dvmptfsum  23738  plyss  23955  nbuhgr  26239  chsupunss  28203  shsupunss  28205  spanss  28207  shslubi  28244  shlub  28273  mdsl1i  29180  mdsl2i  29181  cvmdi  29183  mdslmd1lem1  29184  mdslmd1lem2  29185  mdslmd2i  29189  mdslmd4i  29192  atomli  29241  atcvatlem  29244  chirredlem2  29250  chirredi  29253  mdsymlem5  29266  xrge0infss  29525  tpr2rico  29958  sigainb  30199  dya2icoseg2  30340  omssubadd  30362  eulerpartlemn  30443  ballotlem2  30550  cvmlift2lem12  31296  opnbnd  32320  fneint  32343  bj-intss  33053  dissneqlem  33187  fin2so  33396  matunitlindflem1  33405  mblfinlem4  33449  ismblfin  33450  filbcmb  33535  heiborlem10  33619  igenmin  33863  lssatle  34302  paddss1  35103  paddss2  35104  paddss12  35105  paddssw2  35130  pclssN  35180  pclfinN  35186  polsubN  35193  2polvalN  35200  2polssN  35201  3polN  35202  2pmaplubN  35212  pnonsingN  35219  polsubclN  35238  dihord6apre  36545  dochsscl  36657  mapdordlem2  36926  isnacs3  37273  itgoss  37733  sspwimp  39154  sspwimpVD  39155  nsstr  39273  islptre  39851  gsumlsscl  42164  lincellss  42215  ellcoellss  42224