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

Hypotheses  eqnetrr.1   A = B 

eqnetrr.2   A =/= C 

Assertion  eqnetrri   B =/= C 
Step  Hyp  Ref  Expression 

1  eqnetrr.1   A = B 

2  eqnetrr.2   A =/= C 

3  1  eqcomi   B = A 
4  3 2  eqnetri   B =/= C 