Theorem sstr 3236

Description: Transitivity of subclasses. Theorem 6 of [Suppes] p. 23. (Contributed by NM, 5-Sep-2003.)

Assertion

Ref	Expression
sstr	|- ( ( A C_ B /\ B C_ C ) -> A C_ C )

Proof of Theorem sstr

Step	Hyp	Ref	Expression
1		sstr2 3235	. 2 |- ( A C_ B -> ( B C_ C -> A C_ C ) )
2	1	imp 124	1 |- ( ( A C_ B /\ B C_ C ) -> A C_ C )

Syntax hints:   -> wi 4   /\ wa 104   C_ wss 3201

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  sstrd  3238  sylan9ss  3241  ssdifss  3339  uneqin  3460  ssindif0im  3556  undifss  3577  ssrnres  5186  relrelss  5270  fco  5507  fssres  5520  ssimaex  5716  fcof  5841  tpostpos2  6474  smores  6501  pmss12g  6887  fidcenumlemr  7197  iccsupr  10245  fimaxq  11137  fsum2d  12059  fsumabs  12089  fprod2d  12247  tgval  13408  tgvalex  13409  subrngintm  14290  subrgintm  14321  ssnei  14945  opnneiss  14952  restdis  14978  tgcnp  15003  blssexps  15223  blssex  15224  mopni3  15278  metss  15288  metcnp3  15305  tgioo  15348  cncfmptid  15391  dvmptfsum  15519  plyss  15532