Description: Inference for inequality. (Contributed by NM, 29Apr2005) (Proof shortened by Wolf Lammen, 19Nov2019)
Ref  Expression  

Hypothesis  neeq1i.1   A = B 

Assertion  neeq2i   ( C =/= A <> C =/= B ) 
Step  Hyp  Ref  Expression 

1  neeq1i.1   A = B 

2  1  eqeq2i   ( C = A <> C = B ) 
3  2  necon3bii   ( C =/= A <> C =/= B ) 