Theorem sstr 3938

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ⊆ wss 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ss 3915

This theorem is used by:  sstrd  3940  sylan9ss  3943  ssdifss  4086  uneqin  4234  intss2  5067  ssrnres  6165  relrelss  6264  fcof  6721  fssres  6736  ssimaex  6958  dff3  7088  tpostpos2  8242  smores  8338  om00  8561  omeulem2  8569  cofonr  8661  naddunif  8681  pmss12g  8875  fissorduni  9260  unblem1  9262  unblem2  9263  unblem3  9264  unblem4  9265  isfinite2  9268  cantnfval2  9648  cantnfle  9650  rankxplim3  9871  hfsshf  9886  hfuni  9895  alephinit  10145  dfac12lem2  10194  ackbij1lem11  10278  cfeq0  10305  cfsuc  10306  cff1  10307  cflim2  10312  cfss  10314  cfslb2n  10317  cofsmo  10318  cfsmolem  10319  fin23lem34  10395  fin1a2lem13  10461  axdc3lem2  10500  axdclem  10568  pwcfsdom  10639  wunfi  10777  tskxpss  10828  tskcard  10837  suprzcl  12748  uzwo  13007  uzwo2  13008  infssuzle  13027  infssuzcl  13028  supxrbnd  13427  supxrgtmnf  13428  supxrre1  13429  supxrre2  13430  supxrss  13431  infxrss  13439  iccsupr  13542  hashf1lem2  14568  trclun  15134  fsum2d  15904  fsumabs  15935  fsumrlim  15945  fsumo1  15946  fprod2d  16115  rpnnen2lem4  16352  rpnnen2lem7  16355  ramub2  17153  ressinbas  17384  ressress  17386  submre  17736  mrcss  17751  mreacs  17793  drsdirfi  18440  clatglbss  18654  ipopos  18671  chnrdss  18752  cntz2ss  19510  pgrpsubgsymg  19584  ablfac1eulem  20249  subrngint  20773  subrgint  20808  matunitlindflem1  22955  tgval  23234  mretopd  23371  ssnei  23389  opnneiss  23397  restdis  23457  restcls  23460  restntr  23461  tgcnp  23532  fbssfi  24117  fgss2  24154  fgcl  24158  supfil  24175  alexsubALTlem3  24329  alexsubALTlem4  24330  cnextcn  24347  ustex3sym  24498  trust  24509  restutop  24517  utop2nei  24530  cfiluweak  24574  blssexps  24706  blssex  24707  mopni3  24774  metss  24788  metcnp3  24820  metust  24838  cfilucfil  24839  psmetutop  24847  tgioo  25076  xrsmopn  25093  fsumcn  25152  cncfmptid  25195  iscmet3lem2  25574  caussi  25579  ovolsslem  25766  ovolsscl  25768  ovolssnul  25769  opnmblALT  25885  itgfsum  26108  limcresi  26166  dvmptfsum  26256  plyss  26478  madebdayim  28207  cofcutrtime  28246  n0fincut  28674  nbuhgr  29857  chsupunss  31879  shsupunss  31881  spanss  31883  shslubi  31920  shlub  31949  mdsl1i  32856  mdsl2i  32857  cvmdi  32859  mdslmd1lem1  32860  mdslmd1lem2  32861  mdslmd2i  32865  mdslmd4i  32868  atomli  32917  atcvatlem  32920  chirredlem2  32926  chirredi  32929  mdsymlem5  32942  xrge0infss  33285  tpr2rico  34477  sigainb  34702  dya2icoseg2  34844  omssubadd  34866  eulerpartlemn  34947  ballotlem2  35055  nummin  35652  cvmlift2lem12  36000  opnbnd  37035  fneint  37058  ttcss2  37209  ssttctr  37214  dissneqlem  38183  inunissunidif  38218  pibt2  38260  fin2so  38450  mblfinlem4  38498  ismblfin  38499  filbcmb  38594  heiborlem10  38674  igenmin  38918  lssatle  39992  paddss1  40794  paddss2  40795  paddss12  40796  paddssw2  40821  pclssN  40871  pclfinN  40877  polsubN  40884  2polvalN  40891  2polssN  40892  3polN  40893  2pmaplubN  40903  pnonsingN  40910  polsubclN  40929  dihord6apre  42233  dochsscl  42345  mapdordlem2  42614  isnacs3  43659  itgoss  44108  ofoaid1  44303  ofoaid2  44304  sspwimp  45844  sspwimpVD  45845  nsstr  46031  islptre  46553  gsumlsscl  49414  lincellss  49460  ellcoellss  49469