Theorem necon4bd 2949

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2929

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 2930

This theorem is referenced by:  iftrueb  4487  om00  8496  pw2f1olem  9001  xlt2add  13161  hashfun  14346  hashtpg  14394  fsumcl2lem  15640  fprodcl2lem  15859  gcdeq0  16430  lcmeq0  16513  lcmfeq0b  16543  phibndlem  16683  abvn0b  20753  cfinufil  23844  isxmet2d  24243  i1fres  25634  tdeglem4  25993  ply1domn  26057  pilem2  26390  isnsqf  27073  ppieq0  27114  chpeq0  27147  chteq0  27148  ltrnatlw  40303  bcc0  44458