Theorem necon4bd 2963

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2943

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 2944

This theorem is referenced by:  om00  8394  pw2f1olem  8851  xlt2add  12982  hashfun  14140  hashtpg  14187  fsumcl2lem  15431  fprodcl2lem  15648  gcdeq0  16212  lcmeq0  16293  lcmfeq0b  16323  phibndlem  16459  abvn0b  20561  cfinufil  23067  isxmet2d  23468  i1fres  24858  tdeglem4  25212  tdeglem4OLD  25213  ply1domn  25276  pilem2  25599  isnsqf  26272  ppieq0  26313  chpeq0  26344  chteq0  26345  ltrnatlw  38183  bcc0  41917