Theorem necon4bd 2949

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1533   ≠ wne 2929

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 206  df-ne 2930

This theorem is referenced by:  om00  8596  pw2f1olem  9101  xlt2add  13274  hashfun  14432  hashtpg  14482  fsumcl2lem  15713  fprodcl2lem  15930  gcdeq0  16495  lcmeq0  16574  lcmfeq0b  16604  phibndlem  16742  abvn0b  21269  cfinufil  23876  isxmet2d  24277  i1fres  25679  tdeglem4  26039  tdeglem4OLD  26040  ply1domn  26104  pilem2  26434  isnsqf  27112  ppieq0  27153  chpeq0  27186  chteq0  27187  ltrnatlw  39783  bcc0  43916