Metamath Proof Explorer
Description: Contrapositive inference for inequality. (Contributed by NM, 13Apr2007)


Ref 
Expression 

Hypothesis 
necon2bbii.1 
 ( ph <> A =/= B ) 

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

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

bicomi 
 ( A =/= B <> ph ) 
3 
2

necon1bbii 
 ( . ph <> A = B ) 
4 
3

bicomi 
 ( A = B <> . ph ) 