Theorem sstr 3233

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

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

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211

This theorem is referenced by:  sstrd  3235  sylan9ss  3238  ssdifss  3335  uneqin  3456  ssindif0im  3552  undifss  3573  ssrnres  5177  relrelss  5261  fco  5497  fssres  5509  ssimaex  5703  fcof  5828  tpostpos2  6426  smores  6453  pmss12g  6839  fidcenumlemr  7148  iccsupr  10194  fimaxq  11084  fsum2d  11989  fsumabs  12019  fprod2d  12177  tgval  13338  tgvalex  13339  subrngintm  14219  subrgintm  14250  ssnei  14868  opnneiss  14875  restdis  14901  tgcnp  14926  blssexps  15146  blssex  15147  mopni3  15201  metss  15211  metcnp3  15228  tgioo  15271  cncfmptid  15314  dvmptfsum  15442  plyss  15455