Theorem necon4bd 2964

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

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

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 2945

This theorem is referenced by:  om00  8382  pw2f1olem  8832  xlt2add  12976  hashfun  14133  hashtpg  14180  fsumcl2lem  15424  fprodcl2lem  15641  gcdeq0  16205  lcmeq0  16286  lcmfeq0b  16316  phibndlem  16452  abvn0b  20554  cfinufil  23060  isxmet2d  23461  i1fres  24851  tdeglem4  25205  tdeglem4OLD  25206  ply1domn  25269  pilem2  25592  isnsqf  26265  ppieq0  26306  chpeq0  26337  chteq0  26338  ltrnatlw  38176  bcc0  41911