Theorem necon4bd 2976

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1559   ≠ wne 2956

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 209  df-ne 2957

This theorem is referenced by:  iftrueb  4492  om00  8539  pw2f1olem  9049  xlt2add  13260  hashfun  14447  hashtpg  14495  fsumcl2lem  15741  fprodcl2lem  15963  gcdeq0  16534  lcmeq0  16617  lcmfeq0b  16647  phibndlem  16788  abvn0b  20865  cfinufil  23968  isxmet2d  24367  i1fres  25747  tdeglem4  26100  ply1domn  26164  pilem2  26492  isnsqf  27176  ppieq0  27217  chpeq0  27249  chteq0  27250  ltrnatlw  40771  bcc0  44880