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

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

3netr3g.2   A = C 

3netr3g.3   B = D 

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

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

2  3netr3g.2   A = C 

3  3netr3g.3   B = D 

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