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


Ref 
Expression 

Hypothesis 
necon2i.1 
 ( A = B > C =/= D ) 

Assertion 
necon2i 
 ( C = D > A =/= B ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

necon2i.1 
 ( A = B > C =/= D ) 
2 
1

neneqd 
 ( A = B > . C = D ) 
3 
2

necon2ai 
 ( C = D > A =/= B ) 