Theorem sstr 3188

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

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

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 3160  df-ss 3167

This theorem is referenced by:  sstrd  3190  sylan9ss  3193  ssdifss  3290  uneqin  3411  ssindif0im  3507  undifss  3528  ssrnres  5109  relrelss  5193  fco  5420  fssres  5430  ssimaex  5619  tpostpos2  6320  smores  6347  pmss12g  6731  fidcenumlemr  7016  iccsupr  10035  fimaxq  10901  fsum2d  11581  fsumabs  11611  fprod2d  11769  tgval  12876  tgvalex  12877  subrngintm  13711  subrgintm  13742  ssnei  14330  opnneiss  14337  restdis  14363  tgcnp  14388  blssexps  14608  blssex  14609  mopni3  14663  metss  14673  metcnp3  14690  tgioo  14733  cncfmptid  14776  dvmptfsum  14904  plyss  14917