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


Ref 
Expression 

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

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

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

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

necon1abii 
 ( A =/= B <> ph ) 
4 
3

bicomi 
 ( ph <> A =/= B ) 