Metamath Proof Explorer
Description: Deduction from equality to inequality. (Contributed by NM, 13Apr2007)


Ref 
Expression 

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

Assertion 
necon3bbii 
 ( . ph <> A =/= B ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

necon3bbii.1 
 ( ph <> A = B ) 
2 
1

bicomi 
 ( A = B <> ph ) 
3 
2

necon3abii 
 ( A =/= B <> . ph ) 
4 
3

bicomi 
 ( . ph <> A =/= B ) 