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 1540   ≠ 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  4513  om00  8587  pw2f1olem  9090  xlt2add  13276  hashfun  14455  hashtpg  14503  fsumcl2lem  15747  fprodcl2lem  15966  gcdeq0  16536  lcmeq0  16619  lcmfeq0b  16649  phibndlem  16789  abvn0b  20796  cfinufil  23866  isxmet2d  24266  i1fres  25658  tdeglem4  26017  ply1domn  26081  pilem2  26414  isnsqf  27097  ppieq0  27138  chpeq0  27171  chteq0  27172  ltrnatlw  40202  bcc0  44364