Metamath Proof Explorer
Description: Contrapositive law deduction for inequality. (Contributed by NM, 2Apr2007) (Proof shortened by Andrew Salmon, 25May2011)


Ref 
Expression 

Hypothesis 
necon3bd.1 
⊢ ( 𝜑 → ( 𝐴 = 𝐵 → 𝜓 ) ) 

Assertion 
necon3bd 
⊢ ( 𝜑 → ( ¬ 𝜓 → 𝐴 ≠ 𝐵 ) ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

necon3bd.1 
⊢ ( 𝜑 → ( 𝐴 = 𝐵 → 𝜓 ) ) 
2 

nne 
⊢ ( ¬ 𝐴 ≠ 𝐵 ↔ 𝐴 = 𝐵 ) 
3 
2 1

syl5bi 
⊢ ( 𝜑 → ( ¬ 𝐴 ≠ 𝐵 → 𝜓 ) ) 
4 
3

con1d 
⊢ ( 𝜑 → ( ¬ 𝜓 → 𝐴 ≠ 𝐵 ) ) 