Theorem necon4bd 2955

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ≠ wne 2935

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 208  df-ne 2936

This theorem is referenced by:  iftrueb  4474  om00  8507  pw2f1olem  9016  xlt2add  13210  hashfun  14397  hashtpg  14445  fsumcl2lem  15691  fprodcl2lem  15913  gcdeq0  16484  lcmeq0  16567  lcmfeq0b  16597  phibndlem  16738  abvn0b  20815  cfinufil  23918  isxmet2d  24317  i1fres  25697  tdeglem4  26050  ply1domn  26114  pilem2  26442  isnsqf  27123  ppieq0  27164  chpeq0  27196  chteq0  27197  ltrnatlw  40682  bcc0  44791