Theorem necon4bd 2960

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 2956	. 2 ⊢ (𝜑 → (𝐴 = 𝐵 → ¬ ¬ 𝜓))
3		notnotr 130	. 2 ⊢ (¬ ¬ 𝜓 → 𝜓)
4	2, 3	syl6 35	1 ⊢ (𝜑 → (𝐴 = 𝐵 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2940

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 207  df-ne 2941

This theorem is referenced by:  iftrueb  4538  om00  8613  pw2f1olem  9116  xlt2add  13302  hashfun  14476  hashtpg  14524  fsumcl2lem  15767  fprodcl2lem  15986  gcdeq0  16554  lcmeq0  16637  lcmfeq0b  16667  phibndlem  16807  abvn0b  20837  cfinufil  23936  isxmet2d  24337  i1fres  25740  tdeglem4  26099  ply1domn  26163  pilem2  26496  isnsqf  27178  ppieq0  27219  chpeq0  27252  chteq0  27253  ltrnatlw  40185  bcc0  44359