Theorem necon4bd 2961

Description: Contrapositive inference for inequality. (Contributed by NM, 1-Jun-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)

Hypothesis

Ref	Expression
necon4bd.1	⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵))

Assertion

Ref	Expression
necon4bd	⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))

Proof of Theorem necon4bd

Step	Hyp	Ref	Expression
1		necon4bd.1	. . 3 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 ≠ 𝐵))
2	1	necon2bd 2957	. 2 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ ¬ 𝜓))
3		notnotr 130	. 2 ⊢ (¬ ¬ 𝜓 → 𝜓)
4	2, 3	syl6 35	1 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-ne 2942

This theorem is referenced by:  om00  8575  pw2f1olem  9076  xlt2add  13239  hashfun  14397  hashtpg  14446  fsumcl2lem  15677  fprodcl2lem  15894  gcdeq0  16458  lcmeq0  16537  lcmfeq0b  16567  phibndlem  16703  abvn0b  20920  cfinufil  23432  isxmet2d  23833  i1fres  25223  tdeglem4  25577  tdeglem4OLD  25578  ply1domn  25641  pilem2  25964  isnsqf  26639  ppieq0  26680  chpeq0  26711  chteq0  26712  ltrnatlw  39054  bcc0  43099