Description: Subclass transitivity deduction. (Contributed by NM, 2Jun2004)
Ref  Expression  

Hypotheses  sstrd.1   ( ph > A C_ B ) 

sstrd.2   ( ph > B C_ C ) 

Assertion  sstrd   ( ph > A C_ C ) 
Step  Hyp  Ref  Expression 

1  sstrd.1   ( ph > A C_ B ) 

2  sstrd.2   ( ph > B C_ C ) 

3  sstr   ( ( A C_ B /\ B C_ C ) > A C_ C ) 

4  1 2 3  syl2anc   ( ph > A C_ C ) 