Theorem necon4bd 2802

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ≠ wne 2780

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 196  df-ne 2782

This theorem is referenced by:  om00  7542  pw2f1olem  7949  xlt2add  11962  hashfun  13084  hashtpg  13121  fsumcl2lem  14309  fprodcl2lem  14519  gcdeq0  15076  lcmeq0  15151  lcmfeq0b  15181  phibndlem  15313  abvn0b  19123  cfinufil  21542  isxmet2d  21942  i1fres  23278  tdeglem4  23624  ply1domn  23687  pilem2  24010  isnsqf  24661  ppieq0  24702  chpeq0  24733  chteq0  24734  ltrnatlw  34488  bcc0  37561