Theorem sstr 3234

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

Syntax hints:   → wi 4   ∧ wa 104   ⊆ wss 3199

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-in 3205  df-ss 3212

This theorem is referenced by:  sstrd  3236  sylan9ss  3239  ssdifss  3336  uneqin  3457  ssindif0im  3553  undifss  3574  ssrnres  5181  relrelss  5265  fco  5502  fssres  5514  ssimaex  5710  fcof  5836  tpostpos2  6436  smores  6463  pmss12g  6849  fidcenumlemr  7159  iccsupr  10206  fimaxq  11097  fsum2d  12019  fsumabs  12049  fprod2d  12207  tgval  13368  tgvalex  13369  subrngintm  14250  subrgintm  14281  ssnei  14904  opnneiss  14911  restdis  14937  tgcnp  14962  blssexps  15182  blssex  15183  mopni3  15237  metss  15247  metcnp3  15264  tgioo  15307  cncfmptid  15350  dvmptfsum  15478  plyss  15491