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

Hypothesis  neeq1i.1   A = B 

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

1  neeq1i.1   A = B 

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