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


Ref 
Expression 

Hypothesis 
necon3i.1 
⊢ ( 𝐴 = 𝐵 → 𝐶 = 𝐷 ) 

Assertion 
necon3i 
⊢ ( 𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵 ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

necon3i.1 
⊢ ( 𝐴 = 𝐵 → 𝐶 = 𝐷 ) 
2 
1

necon3ai 
⊢ ( 𝐶 ≠ 𝐷 → ¬ 𝐴 = 𝐵 ) 
3 
2

neqned 
⊢ ( 𝐶 ≠ 𝐷 → 𝐴 ≠ 𝐵 ) 