Theorem sstr 3931

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

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

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

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

This theorem is referenced by:  sstrd  3933  sylan9ss  3936  ssdifss  4081  uneqin  4230  intss2  5051  ssrnres  6134  relrelss  6229  fcof  6683  fssres  6698  ssimaex  6917  dff3  7044  tpostpos2  8188  smores  8283  om00  8501  omeulem2  8509  cofonr  8601  naddunif  8620  pmss12g  8808  unblem1  9193  unblem2  9194  unblem3  9195  unblem4  9196  isfinite2  9199  cantnfval2  9579  cantnfle  9581  rankxplim3  9794  alephinit  10006  dfac12lem2  10056  ackbij1lem11  10140  cfeq0  10167  cfsuc  10168  cff1  10169  cflim2  10174  cfss  10176  cfslb2n  10179  cofsmo  10180  cfsmolem  10181  fin23lem34  10257  fin1a2lem13  10323  axdc3lem2  10362  axdclem  10430  pwcfsdom  10495  wunfi  10633  tskxpss  10684  tskcard  10693  suprzcl  12573  uzwo  12825  uzwo2  12826  infssuzle  12845  infssuzcl  12846  supxrbnd  13244  supxrgtmnf  13245  supxrre1  13246  supxrre2  13247  supxrss  13248  infxrss  13256  iccsupr  13359  hashf1lem2  14380  trclun  14938  fsum2d  15695  fsumabs  15725  fsumrlim  15735  fsumo1  15736  fprod2d  15905  rpnnen2lem4  16143  rpnnen2lem7  16146  ramub2  16943  ressinbas  17173  ressress  17175  submre  17525  mrcss  17540  mreacs  17582  drsdirfi  18229  clatglbss  18443  ipopos  18460  chnrdss  18541  cntz2ss  19268  pgrpsubgsymg  19342  ablfac1eulem  20007  subrngint  20495  subrgint  20530  tgval  22898  mretopd  23035  ssnei  23053  opnneiss  23061  restdis  23121  restcls  23124  restntr  23125  tgcnp  23196  fbssfi  23780  fgss2  23817  fgcl  23821  supfil  23838  alexsubALTlem3  23992  alexsubALTlem4  23993  cnextcn  24010  ustex3sym  24161  trust  24172  restutop  24180  utop2nei  24193  cfiluweak  24237  blssexps  24369  blssex  24370  mopni3  24437  metss  24451  metcnp3  24483  metust  24501  cfilucfil  24502  psmetutop  24510  tgioo  24739  xrsmopn  24756  fsumcn  24815  cncfmptid  24858  iscmet3lem2  25237  caussi  25242  ovolsslem  25429  ovolsscl  25431  ovolssnul  25432  opnmblALT  25548  itgfsum  25772  limcresi  25830  dvmptfsum  25920  plyss  26145  madebdayim  27868  cofcutrtime  27907  n0fincut  28335  nbuhgr  29400  chsupunss  31404  shsupunss  31406  spanss  31408  shslubi  31445  shlub  31474  mdsl1i  32381  mdsl2i  32382  cvmdi  32384  mdslmd1lem1  32385  mdslmd1lem2  32386  mdslmd2i  32390  mdslmd4i  32393  atomli  32442  atcvatlem  32445  chirredlem2  32451  chirredi  32454  mdsymlem5  32467  xrge0infss  32823  tpr2rico  34062  sigainb  34286  dya2icoseg2  34428  omssubadd  34450  eulerpartlemn  34531  ballotlem2  34639  fissorduni  35239  nummin  35242  cvmlift2lem12  35502  opnbnd  36513  fneint  36536  ttcss2  36687  ssttctr  36692  dissneqlem  37652  inunissunidif  37687  pibt2  37729  fin2so  37919  matunitlindflem1  37928  mblfinlem4  37972  ismblfin  37973  filbcmb  38052  heiborlem10  38132  igenmin  38376  lssatle  39452  paddss1  40254  paddss2  40255  paddss12  40256  paddssw2  40281  pclssN  40331  pclfinN  40337  polsubN  40344  2polvalN  40351  2polssN  40352  3polN  40353  2pmaplubN  40363  pnonsingN  40370  polsubclN  40389  dihord6apre  41693  dochsscl  41805  mapdordlem2  42074  isnacs3  43141  itgoss  43594  ofoaid1  43789  ofoaid2  43790  sspwimp  45347  sspwimpVD  45348  nsstr  45528  islptre  46053  gsumlsscl  48814  lincellss  48860  ellcoellss  48869