Theorem necon4bd 3036

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 3016

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 3017

This theorem is referenced by:  om00  8201  pw2f1olem  8621  xlt2add  12654  hashfun  13799  hashtpg  13844  fsumcl2lem  15088  fprodcl2lem  15304  gcdeq0  15865  lcmeq0  15944  lcmfeq0b  15974  phibndlem  16107  abvn0b  20075  cfinufil  22536  isxmet2d  22937  i1fres  24306  tdeglem4  24654  ply1domn  24717  pilem2  25040  isnsqf  25712  ppieq0  25753  chpeq0  25784  chteq0  25785  ltrnatlw  37334  bcc0  40692