Theorem sstr 3977

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

Syntax hints:   → wi 4   ∧ wa 398   ⊆ wss 3938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-in 3945  df-ss 3954

This theorem is referenced by:  sstrd  3979  sylan9ss  3982  ssdifss  4114  uneqin  4257  ssrnres  6037  relrelss  6126  fco  6533  fssres  6546  ssimaex  6750  dff3  6868  tpostpos2  7915  smores  7991  om00  8203  omeulem2  8211  pmss12g  8435  unblem1  8772  unblem2  8773  unblem3  8774  unblem4  8775  isfinite2  8778  cantnfval2  9134  cantnfle  9136  rankxplim3  9312  alephinit  9523  dfac12lem2  9572  ackbij1lem11  9654  cfeq0  9680  cfsuc  9681  cff1  9682  cflim2  9687  cfss  9689  cfslb2n  9692  cofsmo  9693  cfsmolem  9694  fin23lem34  9770  fin1a2lem13  9836  axdc3lem2  9875  axdclem  9943  pwcfsdom  10007  wunfi  10145  tskxpss  10196  tskcard  10205  suprzcl  12065  uzwo  12314  uzwo2  12315  infssuzle  12334  infssuzcl  12335  supxrbnd  12724  supxrgtmnf  12725  supxrre1  12726  supxrre2  12727  supxrss  12728  infxrss  12735  iccsupr  12833  hashf1lem2  13817  trclun  14376  fsum2d  15128  fsumabs  15158  fsumrlim  15168  fsumo1  15169  fprod2d  15337  rpnnen2lem4  15572  rpnnen2lem7  15575  ramub2  16352  ressinbas  16562  ressress  16564  submre  16878  mrcss  16889  mreacs  16931  drsdirfi  17550  clatglbss  17739  ipopos  17772  cntz2ss  18465  pgrpsubgsymg  18539  ablfac1eulem  19196  subrgint  19559  tgval  21565  mretopd  21702  ssnei  21720  opnneiss  21728  restdis  21788  restcls  21791  restntr  21792  tgcnp  21863  fbssfi  22447  fgss2  22484  fgcl  22488  supfil  22505  alexsubALTlem3  22659  alexsubALTlem4  22660  cnextcn  22677  ustex3sym  22828  trust  22840  restutop  22848  utop2nei  22861  cfiluweak  22906  blssexps  23038  blssex  23039  mopni3  23106  metss  23120  metcnp3  23152  metust  23170  cfilucfil  23171  psmetutop  23179  tgioo  23406  xrsmopn  23422  fsumcn  23480  cncfmptid  23522  iscmet3lem2  23897  caussi  23902  ovolsslem  24087  ovolsscl  24089  ovolssnul  24090  opnmblALT  24206  itgfsum  24429  limcresi  24485  dvmptfsum  24574  plyss  24791  nbuhgr  27127  chsupunss  29123  shsupunss  29125  spanss  29127  shslubi  29164  shlub  29193  mdsl1i  30100  mdsl2i  30101  cvmdi  30103  mdslmd1lem1  30104  mdslmd1lem2  30105  mdslmd2i  30109  mdslmd4i  30112  atomli  30161  atcvatlem  30164  chirredlem2  30170  chirredi  30173  mdsymlem5  30186  xrge0infss  30486  tpr2rico  31157  sigainb  31397  dya2icoseg2  31538  omssubadd  31560  eulerpartlemn  31641  ballotlem2  31748  cvmlift2lem12  32563  opnbnd  33675  fneint  33698  bj-intss  34393  dissneqlem  34623  inunissunidif  34658  pibt2  34700  fin2so  34881  matunitlindflem1  34890  mblfinlem4  34934  ismblfin  34935  filbcmb  35017  heiborlem10  35100  igenmin  35344  lssatle  36153  paddss1  36955  paddss2  36956  paddss12  36957  paddssw2  36982  pclssN  37032  pclfinN  37038  polsubN  37045  2polvalN  37052  2polssN  37053  3polN  37054  2pmaplubN  37064  pnonsingN  37071  polsubclN  37090  dihord6apre  38394  dochsscl  38506  mapdordlem2  38775  isnacs3  39314  itgoss  39770  sspwimp  41259  sspwimpVD  41260  nsstr  41368  islptre  41907  gsumlsscl  44438  lincellss  44488  ellcoellss  44497