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

Hypotheses  neeqtr.1   A =/= B 

neeqtr.2   B = C 

Assertion  neeqtri   A =/= C 
Step  Hyp  Ref  Expression 

1  neeqtr.1   A =/= B 

2  neeqtr.2   B = C 

3  2  neeq2i   ( A =/= B <> A =/= C ) 
4  1 3  mpbi   A =/= C 