Theorem sstr 3575

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

Syntax hints:   → wi 4   ∧ wa 382   ⊆ wss 3539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-in 3546  df-ss 3553

This theorem is referenced by:  sstrd  3577  sylan9ss  3580  ssdifss  3702  uneqin  3836  ssrnres  5477  relrelss  5562  fco  5957  fssres  5968  ssimaex  6158  dff3  6265  tpostpos2  7237  smores  7313  om00  7519  omeulem2  7527  pmss12g  7747  unblem1  8074  unblem2  8075  unblem3  8076  unblem4  8077  isfinite2  8080  cantnfval2  8426  cantnfle  8428  rankxplim3  8604  alephinit  8778  dfac12lem2  8826  ackbij1lem11  8912  cfeq0  8938  cfsuc  8939  cff1  8940  cflim2  8945  cfss  8947  cfslb2n  8950  cofsmo  8951  cfsmolem  8952  fin23lem34  9028  fin1a2lem13  9094  axdc3lem2  9133  axdclem  9201  pwcfsdom  9261  wunfi  9399  tskxpss  9450  tskcard  9459  suprzcl  11289  uzwo  11583  uzwo2  11584  infssuzle  11603  infssuzcl  11604  supxrbnd  11986  supxrgtmnf  11987  supxrre1  11988  supxrre2  11989  supxrss  11990  infxrss  11996  iccsupr  12093  hashf1lem2  13049  trclun  13549  fsum2d  14290  fsumabs  14320  fsumrlim  14330  fsumo1  14331  fprod2d  14496  rpnnen2lem4  14731  rpnnen2lem7  14734  ramub2  15502  ressinbas  15709  ressress  15711  submre  16034  mrcss  16045  mreacs  16088  drsdirfi  16707  clatglbss  16896  ipopos  16929  cntz2ss  17534  ablfac1eulem  18240  subrgint  18571  tgval  20512  mretopd  20648  ssnei  20666  opnneiss  20674  restdis  20734  restcls  20737  restntr  20738  tgcnp  20809  fbssfi  21393  fgss2  21430  fgcl  21434  supfil  21451  alexsubALTlem3  21605  alexsubALTlem4  21606  cnextcn  21623  ustex3sym  21773  trust  21785  restutop  21793  utop2nei  21806  cfiluweak  21851  blssexps  21982  blssex  21983  mopni3  22050  metss  22064  metcnp3  22096  metust  22114  cfilucfil  22115  psmetutop  22123  tgioo  22339  xrsmopn  22355  fsumcn  22412  cncfmptid  22454  iscmet3lem2  22816  caussi  22821  ovolsslem  22976  ovolsscl  22978  ovolssnul  22979  opnmblALT  23094  itgfsum  23316  limcresi  23372  dvmptfsum  23459  plyss  23676  chsupunss  27393  shsupunss  27395  spanss  27397  shslubi  27434  shlub  27463  mdsl1i  28370  mdsl2i  28371  cvmdi  28373  mdslmd1lem1  28374  mdslmd1lem2  28375  mdslmd2i  28379  mdslmd4i  28382  atomli  28431  atcvatlem  28434  chirredlem2  28440  chirredi  28443  mdsymlem5  28456  xrge0infss  28721  tpr2rico  29092  sigainb  29332  dya2icoseg2  29473  omssubadd  29495  eulerpartlemn  29576  ballotlem2  29683  cvmlift2lem12  30356  opnbnd  31296  fneint  31319  dissneqlem  32159  fin2so  32362  matunitlindflem1  32371  mblfinlem4  32415  ismblfin  32416  filbcmb  32501  heiborlem10  32585  igenmin  32829  lssatle  33116  paddss1  33917  paddss2  33918  paddss12  33919  paddssw2  33944  pclssN  33994  pclfinN  34000  polsubN  34007  2polvalN  34014  2polssN  34015  3polN  34016  2pmaplubN  34026  pnonsingN  34033  polsubclN  34052  dihord6apre  35359  dochsscl  35471  mapdordlem2  35740  isnacs3  36087  itgoss  36548  sspwimp  37972  sspwimpVD  37973  nsstr  38097  islptre  38483  nbuhgr  40560  gsumlsscl  41953  lincellss  42004  ellcoellss  42013