Theorem necon4bd 2961

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2941

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 206  df-ne 2942

This theorem is referenced by:  om00  8437  pw2f1olem  8901  xlt2add  13044  hashfun  14201  hashtpg  14248  fsumcl2lem  15492  fprodcl2lem  15709  gcdeq0  16273  lcmeq0  16354  lcmfeq0b  16384  phibndlem  16520  abvn0b  20622  cfinufil  23128  isxmet2d  23529  i1fres  24919  tdeglem4  25273  tdeglem4OLD  25274  ply1domn  25337  pilem2  25660  isnsqf  26333  ppieq0  26374  chpeq0  26405  chteq0  26406  ltrnatlw  38397  bcc0  42171