Theorem sstr 3925

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  sstrd  3927  sylan9ss  3930  ssdifss  4066  uneqin  4209  intss2  5033  ssrnres  6070  relrelss  6165  fcof  6607  fcoOLD  6609  fssres  6624  ssimaex  6835  dff3  6958  tpostpos2  8034  smores  8154  om00  8368  omeulem2  8376  pmss12g  8615  unblem1  8996  unblem2  8997  unblem3  8998  unblem4  8999  isfinite2  9002  cantnfval2  9357  cantnfle  9359  rankxplim3  9570  alephinit  9782  dfac12lem2  9831  ackbij1lem11  9917  cfeq0  9943  cfsuc  9944  cff1  9945  cflim2  9950  cfss  9952  cfslb2n  9955  cofsmo  9956  cfsmolem  9957  fin23lem34  10033  fin1a2lem13  10099  axdc3lem2  10138  axdclem  10206  pwcfsdom  10270  wunfi  10408  tskxpss  10459  tskcard  10468  suprzcl  12330  uzwo  12580  uzwo2  12581  infssuzle  12600  infssuzcl  12601  supxrbnd  12991  supxrgtmnf  12992  supxrre1  12993  supxrre2  12994  supxrss  12995  infxrss  13002  iccsupr  13103  hashf1lem2  14098  trclun  14653  fsum2d  15411  fsumabs  15441  fsumrlim  15451  fsumo1  15452  fprod2d  15619  rpnnen2lem4  15854  rpnnen2lem7  15857  ramub2  16643  ressinbas  16881  ressress  16884  submre  17231  mrcss  17242  mreacs  17284  drsdirfi  17938  clatglbss  18152  ipopos  18169  cntz2ss  18854  pgrpsubgsymg  18932  ablfac1eulem  19590  subrgint  19961  tgval  22013  mretopd  22151  ssnei  22169  opnneiss  22177  restdis  22237  restcls  22240  restntr  22241  tgcnp  22312  fbssfi  22896  fgss2  22933  fgcl  22937  supfil  22954  alexsubALTlem3  23108  alexsubALTlem4  23109  cnextcn  23126  ustex3sym  23277  trust  23289  restutop  23297  utop2nei  23310  cfiluweak  23355  blssexps  23487  blssex  23488  mopni3  23556  metss  23570  metcnp3  23602  metust  23620  cfilucfil  23621  psmetutop  23629  tgioo  23865  xrsmopn  23881  fsumcn  23939  cncfmptid  23982  iscmet3lem2  24361  caussi  24366  ovolsslem  24553  ovolsscl  24555  ovolssnul  24556  opnmblALT  24672  itgfsum  24896  limcresi  24954  dvmptfsum  25044  plyss  25265  nbuhgr  27613  chsupunss  29607  shsupunss  29609  spanss  29611  shslubi  29648  shlub  29677  mdsl1i  30584  mdsl2i  30585  cvmdi  30587  mdslmd1lem1  30588  mdslmd1lem2  30589  mdslmd2i  30593  mdslmd4i  30596  atomli  30645  atcvatlem  30648  chirredlem2  30654  chirredi  30657  mdsymlem5  30670  xrge0infss  30985  tpr2rico  31764  sigainb  32004  dya2icoseg2  32145  omssubadd  32167  eulerpartlemn  32248  ballotlem2  32355  nummin  32963  cvmlift2lem12  33176  madebdayim  33997  cofcutrtime  34020  opnbnd  34441  fneint  34464  dissneqlem  35438  inunissunidif  35473  pibt2  35515  fin2so  35691  matunitlindflem1  35700  mblfinlem4  35744  ismblfin  35745  filbcmb  35825  heiborlem10  35905  igenmin  36149  lssatle  36956  paddss1  37758  paddss2  37759  paddss12  37760  paddssw2  37785  pclssN  37835  pclfinN  37841  polsubN  37848  2polvalN  37855  2polssN  37856  3polN  37857  2pmaplubN  37867  pnonsingN  37874  polsubclN  37893  dihord6apre  39197  dochsscl  39309  mapdordlem2  39578  isnacs3  40448  itgoss  40904  sspwimp  42427  sspwimpVD  42428  nsstr  42534  islptre  43050  gsumlsscl  45607  lincellss  45655  ellcoellss  45664