Theorem sstr 3233

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 3232	. 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 3198

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211

This theorem is referenced by:  sstrd  3235  sylan9ss  3238  ssdifss  3335  uneqin  3456  ssindif0im  3552  undifss  3573  ssrnres  5177  relrelss  5261  fco  5497  fssres  5509  ssimaex  5703  fcof  5828  tpostpos2  6426  smores  6453  pmss12g  6839  fidcenumlemr  7145  iccsupr  10191  fimaxq  11081  fsum2d  11986  fsumabs  12016  fprod2d  12174  tgval  13335  tgvalex  13336  subrngintm  14216  subrgintm  14247  ssnei  14865  opnneiss  14872  restdis  14898  tgcnp  14923  blssexps  15143  blssex  15144  mopni3  15198  metss  15208  metcnp3  15225  tgioo  15268  cncfmptid  15311  dvmptfsum  15439  plyss  15452