Theorem necon4bd 2952

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2932

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 2933

This theorem is referenced by:  iftrueb  4479  om00  8510  pw2f1olem  9019  xlt2add  13212  hashfun  14399  hashtpg  14447  fsumcl2lem  15693  fprodcl2lem  15915  gcdeq0  16486  lcmeq0  16569  lcmfeq0b  16599  phibndlem  16740  abvn0b  20813  cfinufil  23893  isxmet2d  24292  i1fres  25672  tdeglem4  26025  ply1domn  26089  pilem2  26417  isnsqf  27098  ppieq0  27139  chpeq0  27171  chteq0  27172  ltrnatlw  40629  bcc0  44767