Theorem sstr 3903

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

Syntax hints:   → wi 4   ∧ wa 396   ⊆ wss 3865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-in 3872  df-ss 3880

This theorem is referenced by:  sstrd  3905  sylan9ss  3908  ssdifss  4039  uneqin  4181  ssrnres  5918  relrelss  6006  fco  6406  fssres  6419  ssimaex  6622  dff3  6736  tpostpos2  7771  smores  7848  om00  8058  omeulem2  8066  pmss12g  8290  unblem1  8623  unblem2  8624  unblem3  8625  unblem4  8626  isfinite2  8629  cantnfval2  8985  cantnfle  8987  rankxplim3  9163  alephinit  9374  dfac12lem2  9423  ackbij1lem11  9505  cfeq0  9531  cfsuc  9532  cff1  9533  cflim2  9538  cfss  9540  cfslb2n  9543  cofsmo  9544  cfsmolem  9545  fin23lem34  9621  fin1a2lem13  9687  axdc3lem2  9726  axdclem  9794  pwcfsdom  9858  wunfi  9996  tskxpss  10047  tskcard  10056  suprzcl  11916  uzwo  12164  uzwo2  12165  infssuzle  12184  infssuzcl  12185  supxrbnd  12575  supxrgtmnf  12576  supxrre1  12577  supxrre2  12578  supxrss  12579  infxrss  12586  iccsupr  12684  hashf1lem2  13666  trclun  14212  fsum2d  14963  fsumabs  14993  fsumrlim  15003  fsumo1  15004  fprod2d  15172  rpnnen2lem4  15407  rpnnen2lem7  15410  ramub2  16183  ressinbas  16393  ressress  16395  submre  16709  mrcss  16720  mreacs  16762  drsdirfi  17381  clatglbss  17570  ipopos  17603  cntz2ss  18208  ablfac1eulem  18915  subrgint  19251  tgval  21251  mretopd  21388  ssnei  21406  opnneiss  21414  restdis  21474  restcls  21477  restntr  21478  tgcnp  21549  fbssfi  22133  fgss2  22170  fgcl  22174  supfil  22191  alexsubALTlem3  22345  alexsubALTlem4  22346  cnextcn  22363  ustex3sym  22513  trust  22525  restutop  22533  utop2nei  22546  cfiluweak  22591  blssexps  22723  blssex  22724  mopni3  22791  metss  22805  metcnp3  22837  metust  22855  cfilucfil  22856  psmetutop  22864  tgioo  23091  xrsmopn  23107  fsumcn  23165  cncfmptid  23207  iscmet3lem2  23582  caussi  23587  ovolsslem  23772  ovolsscl  23774  ovolssnul  23775  opnmblALT  23891  itgfsum  24114  limcresi  24170  dvmptfsum  24259  plyss  24476  nbuhgr  26812  chsupunss  28808  shsupunss  28810  spanss  28812  shslubi  28849  shlub  28878  mdsl1i  29785  mdsl2i  29786  cvmdi  29788  mdslmd1lem1  29789  mdslmd1lem2  29790  mdslmd2i  29794  mdslmd4i  29797  atomli  29846  atcvatlem  29849  chirredlem2  29855  chirredi  29858  mdsymlem5  29871  xrge0infss  30168  tpr2rico  30768  sigainb  31008  dya2icoseg2  31149  omssubadd  31171  eulerpartlemn  31252  ballotlem2  31359  cvmlift2lem12  32171  opnbnd  33284  fneint  33307  bj-intss  34011  dissneqlem  34173  inunissunidif  34208  pibt2  34250  fin2so  34431  matunitlindflem1  34440  mblfinlem4  34484  ismblfin  34485  filbcmb  34568  heiborlem10  34651  igenmin  34895  lssatle  35703  paddss1  36505  paddss2  36506  paddss12  36507  paddssw2  36532  pclssN  36582  pclfinN  36588  polsubN  36595  2polvalN  36602  2polssN  36603  3polN  36604  2pmaplubN  36614  pnonsingN  36621  polsubclN  36640  dihord6apre  37944  dochsscl  38056  mapdordlem2  38325  isnacs3  38813  itgoss  39269  sspwimp  40812  sspwimpVD  40813  nsstr  40921  islptre  41463  gsumlsscl  43933  lincellss  43983  ellcoellss  43992