Theorem necon4bd 2975

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1569   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2956

This theorem is used by:  iftrueb  4494  om00  8586  pw2f1olem  9103  xlt2add  13393  hashfun  14585  hashtpg  14633  fsumcl2lem  15902  fprodcl2lem  16122  gcdeq0  16694  lcmeq0  16780  lcmfeq0b  16810  phibndlem  16952  abvn0b  21098  cfinufil  24252  isxmet2d  24651  i1fres  26031  tdeglem4  26383  ply1domn  26447  pilem2  26784  isnsqf  27467  ppieq0  27508  chpeq0  27540  chteq0  27541  ltrnatlw  41333  bcc0  45417