Theorem necon4bd 2978

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2958

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 210  df-ne 2959

This theorem is referenced by:  iftrueb  4501  om00  8561  pw2f1olem  9070  xlt2add  13287  hashfun  14476  hashtpg  14524  fsumcl2lem  15784  fprodcl2lem  16006  gcdeq0  16576  lcmeq0  16659  lcmfeq0b  16689  phibndlem  16830  abvn0b  20920  cfinufil  24066  isxmet2d  24465  i1fres  25845  tdeglem4  26198  ply1domn  26262  pilem2  26593  isnsqf  27277  ppieq0  27318  chpeq0  27350  chteq0  27351  ltrnatlw  40935  bcc0  45030