Description: Inference associated with dfne . (Contributed by BJ, 7Jul2018)
Ref  Expression  

Hypothesis  neir.1   . A = B 

Assertion  neir   A =/= B 
Step  Hyp  Ref  Expression 

1  neir.1   . A = B 

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

3  1 2  mpbir   A =/= B 