Theorem necon4bd 2958

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 2938

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 2939

This theorem is referenced by:  om00  8612  pw2f1olem  9115  xlt2add  13299  hashfun  14473  hashtpg  14521  fsumcl2lem  15764  fprodcl2lem  15983  gcdeq0  16551  lcmeq0  16634  lcmfeq0b  16664  phibndlem  16804  abvn0b  20854  cfinufil  23952  isxmet2d  24353  i1fres  25755  tdeglem4  26114  ply1domn  26178  pilem2  26511  isnsqf  27193  ppieq0  27234  chpeq0  27267  chteq0  27268  ltrnatlw  40166  bcc0  44336