Theorem necon4bd 2989

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1601   ≠ wne 2969

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 199  df-ne 2970

This theorem is referenced by:  om00  7939  pw2f1olem  8352  xlt2add  12402  hashfun  13538  hashtpg  13581  fsumcl2lem  14869  fprodcl2lem  15083  gcdeq0  15644  lcmeq0  15719  lcmfeq0b  15749  phibndlem  15879  abvn0b  19699  cfinufil  22140  isxmet2d  22540  i1fres  23909  tdeglem4  24257  ply1domn  24320  pilem2  24643  isnsqf  25313  ppieq0  25354  chpeq0  25385  chteq0  25386  ltrnatlw  36337  bcc0  39495