Theorem necon4bd 2980

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1563   ≠ wne 2960

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 210  df-ne 2961

This theorem is referenced by:  iftrueb  4496  om00  8548  pw2f1olem  9057  xlt2add  13277  hashfun  14464  hashtpg  14512  fsumcl2lem  15772  fprodcl2lem  15994  gcdeq0  16565  lcmeq0  16648  lcmfeq0b  16678  phibndlem  16819  abvn0b  20908  cfinufil  24046  isxmet2d  24445  i1fres  25825  tdeglem4  26178  ply1domn  26242  pilem2  26573  isnsqf  27257  ppieq0  27298  chpeq0  27330  chteq0  27331  ltrnatlw  40819  bcc0  44914