Description: Characterization of inequality in terms of reversed equality (see bicom ). (Contributed by BJ, 7Jul2018)
Ref  Expression  

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

1  eqcom   ( A = B <> B = A ) 

2  1  necon3abii   ( A =/= B <> . B = A ) 