Description: Equality theorem for inequality. (Contributed by NM, 19Nov1994) (Proof shortened by Wolf Lammen, 18Nov2019)
Ref  Expression  

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

1  id   ( A = B > A = B ) 

2  1  neeq2d   ( A = B > ( C =/= A <> C =/= B ) ) 