Description: Subclass transitivity deduction. (Contributed by Jonathan BenNaim, 3Jun2011)
Ref  Expression  

Hypotheses  sstrdi.1   ( ph > A C_ B ) 

sstrdi.2   B C_ C 

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

1  sstrdi.1   ( ph > A C_ B ) 

2  sstrdi.2   B C_ C 

3  2  a1i   ( ph > B C_ C ) 
4  1 3  sstrd   ( ph > A C_ C ) 