Description: Negation of inequality. (Contributed by NM, 9Jun2006)
Ref  Expression  

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

1  dfne   ( A =/= B <> . A = B ) 

2  1  con2bii   ( A = B <> . A =/= B ) 
3  2  bicomi   ( . A =/= B <> A = B ) 