Description: From inequality to nonequality. (Contributed by Glauco Siliprandi, 11Dec2019)
Ref  Expression  

Assertion  neneq   ( A =/= B > . A = B ) 
Step  Hyp  Ref  Expression 

1  id   ( A =/= B > A =/= B ) 

2  1  neneqd   ( A =/= B > . A = B ) 