Description: Substitution of equality into both sides of an inequality. (Contributed by NM, 14Jun2012)
Ref  Expression  

Hypotheses  3netr4g.1   ( ph > A =/= B ) 

3netr4g.2   C = A 

3netr4g.3   D = B 

Assertion  3netr4g   ( ph > C =/= D ) 
Step  Hyp  Ref  Expression 

1  3netr4g.1   ( ph > A =/= B ) 

2  3netr4g.2   C = A 

3  3netr4g.3   D = B 

4  2 3  neeq12i   ( C =/= D <> A =/= B ) 
5  1 4  sylibr   ( ph > C =/= D ) 