Metamath Proof Explorer
Description: Contrapositive inference for inequality. (Contributed by NM, 9Aug2006) (Proof shortened by Wolf Lammen, 22Nov2019)


Ref 
Expression 

Hypothesis 
necon3i.1 
$${\u22a2}{A}={B}\to {C}={D}$$ 

Assertion 
necon3i 
$${\u22a2}{C}\ne {D}\to {A}\ne {B}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

necon3i.1 
$${\u22a2}{A}={B}\to {C}={D}$$ 
2 
1

necon3ai 
$${\u22a2}{C}\ne {D}\to \neg {A}={B}$$ 
3 
2

neqned 
$${\u22a2}{C}\ne {D}\to {A}\ne {B}$$ 