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

Hypotheses  eqnetr.1   A = B 

eqnetr.2   B =/= C 

Assertion  eqnetri   A =/= C 
Step  Hyp  Ref  Expression 

1  eqnetr.1   A = B 

2  eqnetr.2   B =/= C 

3  1  neeq1i   ( A =/= C <> B =/= C ) 
4  2 3  mpbir   A =/= C 