Theorem necon4bd 2960

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

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

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 2941

This theorem is referenced by:  om00  8577  pw2f1olem  9078  xlt2add  13241  hashfun  14399  hashtpg  14448  fsumcl2lem  15679  fprodcl2lem  15896  gcdeq0  16460  lcmeq0  16539  lcmfeq0b  16569  phibndlem  16705  abvn0b  20926  cfinufil  23439  isxmet2d  23840  i1fres  25230  tdeglem4  25584  tdeglem4OLD  25585  ply1domn  25648  pilem2  25971  isnsqf  26646  ppieq0  26687  chpeq0  26718  chteq0  26719  ltrnatlw  39140  bcc0  43181