Theorem sstr 3165

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

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

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3137  df-ss 3144

This theorem is referenced by:  sstrd  3167  sylan9ss  3170  ssdifss  3267  uneqin  3388  ssindif0im  3484  undifss  3505  ssrnres  5073  relrelss  5157  fco  5383  fssres  5393  ssimaex  5579  tpostpos2  6268  smores  6295  pmss12g  6677  fidcenumlemr  6956  iccsupr  9968  fimaxq  10809  fsum2d  11445  fsumabs  11475  fprod2d  11633  tgval  12716  tgvalex  12717  subrgintm  13369  ssnei  13690  opnneiss  13697  restdis  13723  tgcnp  13748  blssexps  13968  blssex  13969  mopni3  14023  metss  14033  metcnp3  14050  tgioo  14085  cncfmptid  14122