Theorem necon4bd 2945

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2925

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 2926

This theorem is referenced by:  iftrueb  4501  om00  8539  pw2f1olem  9045  xlt2add  13220  hashfun  14402  hashtpg  14450  fsumcl2lem  15697  fprodcl2lem  15916  gcdeq0  16487  lcmeq0  16570  lcmfeq0b  16600  phibndlem  16740  abvn0b  20745  cfinufil  23815  isxmet2d  24215  i1fres  25606  tdeglem4  25965  ply1domn  26029  pilem2  26362  isnsqf  27045  ppieq0  27086  chpeq0  27119  chteq0  27120  ltrnatlw  40177  bcc0  44329