Description: Transitivity of subclass relationship. Theorem 6 of Suppes p. 23. (Contributed by NM, 5Sep2003)
Ref  Expression  

Assertion  sstr   ( ( A C_ B /\ B C_ C ) > A C_ C ) 
Step  Hyp  Ref  Expression 

1  sstr2   ( A C_ B > ( B C_ C > A C_ C ) ) 

2  1  imp   ( ( A C_ B /\ B C_ C ) > A C_ C ) 