Description: Deduction from equality to inequality. (Contributed by NM, 9Nov2007)
Ref  Expression  

Hypothesis  necon3abii.1   ( A = B <> ph ) 

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

1  necon3abii.1   ( A = B <> ph ) 

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

3  2 1  xchbinx   ( A =/= B <> . ph ) 