Theorem necon4bd 2945

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

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

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 2926

This theorem is referenced by:  iftrueb  4491  om00  8500  pw2f1olem  9005  xlt2add  13180  hashfun  14362  hashtpg  14410  fsumcl2lem  15656  fprodcl2lem  15875  gcdeq0  16446  lcmeq0  16529  lcmfeq0b  16559  phibndlem  16699  abvn0b  20739  cfinufil  23831  isxmet2d  24231  i1fres  25622  tdeglem4  25981  ply1domn  26045  pilem2  26378  isnsqf  27061  ppieq0  27102  chpeq0  27135  chteq0  27136  ltrnatlw  40162  bcc0  44313