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

Hypothesis  necon3bbid.1   ( ph > ( ps <> A = B ) ) 

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

1  necon3bbid.1   ( ph > ( ps <> A = B ) ) 

2  1  bicomd   ( ph > ( A = B <> ps ) ) 
3  2  necon3abid   ( ph > ( A =/= B <> . ps ) ) 
4  3  bicomd   ( ph > ( . ps <> A =/= B ) ) 