Theorem necon4bd 2977

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

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

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 2958

This theorem is used by:  iftrueb  4498  om00  8566  pw2f1olem  9083  xlt2add  13316  hashfun  14506  hashtpg  14554  fsumcl2lem  15821  fprodcl2lem  16043  gcdeq0  16613  lcmeq0  16696  lcmfeq0b  16726  phibndlem  16867  abvn0b  21008  cfinufil  24160  isxmet2d  24559  i1fres  25939  tdeglem4  26292  ply1domn  26356  pilem2  26695  isnsqf  27379  ppieq0  27420  chpeq0  27452  chteq0  27453  ltrnatlw  41064  bcc0  45172