Theorem necon4bd 3020

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1658   ≠ wne 3000

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 3001

This theorem is referenced by:  om00  7923  pw2f1olem  8334  xlt2add  12379  hashfun  13514  hashtpg  13557  fsumcl2lem  14840  fprodcl2lem  15054  gcdeq0  15612  lcmeq0  15687  lcmfeq0b  15717  phibndlem  15847  abvn0b  19664  cfinufil  22103  isxmet2d  22503  i1fres  23872  tdeglem4  24220  ply1domn  24283  pilem2  24606  isnsqf  25275  ppieq0  25316  chpeq0  25347  chteq0  25348  ltrnatlw  36259  bcc0  39380