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

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

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

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