Theorem sstr 3187

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

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

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3159  df-ss 3166

This theorem is referenced by:  sstrd  3189  sylan9ss  3192  ssdifss  3289  uneqin  3410  ssindif0im  3506  undifss  3527  ssrnres  5108  relrelss  5192  fco  5419  fssres  5429  ssimaex  5618  tpostpos2  6318  smores  6345  pmss12g  6729  fidcenumlemr  7014  iccsupr  10032  fimaxq  10898  fsum2d  11578  fsumabs  11608  fprod2d  11766  tgval  12873  tgvalex  12874  subrngintm  13708  subrgintm  13739  ssnei  14319  opnneiss  14326  restdis  14352  tgcnp  14377  blssexps  14597  blssex  14598  mopni3  14652  metss  14662  metcnp3  14679  tgioo  14714  cncfmptid  14751  plyss  14884