Description: Substitution of equal classes into an inequality. (Contributed by NM, 4Jul2012)
Ref  Expression  

Hypotheses  neeqtrd.1   ( ph > A =/= B ) 

neeqtrd.2   ( ph > B = C ) 

Assertion  neeqtrd   ( ph > A =/= C ) 
Step  Hyp  Ref  Expression 

1  neeqtrd.1   ( ph > A =/= B ) 

2  neeqtrd.2   ( ph > B = C ) 

3  2  neeq2d   ( ph > ( A =/= B <> A =/= C ) ) 
4  1 3  mpbid   ( ph > A =/= C ) 