Theorem necon4bd 2952

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2932

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 2933

This theorem is referenced by:  iftrueb  4492  om00  8502  pw2f1olem  9009  xlt2add  13175  hashfun  14360  hashtpg  14408  fsumcl2lem  15654  fprodcl2lem  15873  gcdeq0  16444  lcmeq0  16527  lcmfeq0b  16557  phibndlem  16697  abvn0b  20769  cfinufil  23872  isxmet2d  24271  i1fres  25662  tdeglem4  26021  ply1domn  26085  pilem2  26418  isnsqf  27101  ppieq0  27142  chpeq0  27175  chteq0  27176  ltrnatlw  40439  bcc0  44577