Theorem necon4bd 2948

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

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

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 207  df-ne 2929

This theorem is referenced by:  iftrueb  4488  om00  8490  pw2f1olem  8994  xlt2add  13159  hashfun  14344  hashtpg  14392  fsumcl2lem  15638  fprodcl2lem  15857  gcdeq0  16428  lcmeq0  16511  lcmfeq0b  16541  phibndlem  16681  abvn0b  20752  cfinufil  23844  isxmet2d  24243  i1fres  25634  tdeglem4  25993  ply1domn  26057  pilem2  26390  isnsqf  27073  ppieq0  27114  chpeq0  27147  chteq0  27148  ltrnatlw  40228  bcc0  44379