Theorem necon4bd 2946

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

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

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 2927

This theorem is referenced by:  iftrueb  4504  om00  8542  pw2f1olem  9050  xlt2add  13227  hashfun  14409  hashtpg  14457  fsumcl2lem  15704  fprodcl2lem  15923  gcdeq0  16494  lcmeq0  16577  lcmfeq0b  16607  phibndlem  16747  abvn0b  20752  cfinufil  23822  isxmet2d  24222  i1fres  25613  tdeglem4  25972  ply1domn  26036  pilem2  26369  isnsqf  27052  ppieq0  27093  chpeq0  27126  chteq0  27127  ltrnatlw  40184  bcc0  44336