Theorem sstr 3202

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

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

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3173  df-ss 3180

This theorem is referenced by:  sstrd  3204  sylan9ss  3207  ssdifss  3304  uneqin  3425  ssindif0im  3521  undifss  3542  ssrnres  5130  relrelss  5214  fco  5447  fssres  5458  ssimaex  5647  tpostpos2  6358  smores  6385  pmss12g  6769  fidcenumlemr  7064  iccsupr  10095  fimaxq  10979  fsum2d  11790  fsumabs  11820  fprod2d  11978  tgval  13138  tgvalex  13139  subrngintm  14018  subrgintm  14049  ssnei  14667  opnneiss  14674  restdis  14700  tgcnp  14725  blssexps  14945  blssex  14946  mopni3  15000  metss  15010  metcnp3  15027  tgioo  15070  cncfmptid  15113  dvmptfsum  15241  plyss  15254