Theorem necon4bd 2814

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1483   ≠ wne 2794

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 197  df-ne 2795

This theorem is referenced by:  om00  7655  pw2f1olem  8064  xlt2add  12090  hashfun  13224  hashtpg  13267  fsumcl2lem  14462  fprodcl2lem  14680  gcdeq0  15238  lcmeq0  15313  lcmfeq0b  15343  phibndlem  15475  abvn0b  19302  cfinufil  21732  isxmet2d  22132  i1fres  23472  tdeglem4  23820  ply1domn  23883  pilem2  24206  isnsqf  24861  ppieq0  24902  chpeq0  24933  chteq0  24934  ltrnatlw  35470  bcc0  38539