Theorem necon4bd 2953

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

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

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 2934

This theorem is referenced by:  iftrueb  4480  om00  8503  pw2f1olem  9012  xlt2add  13203  hashfun  14390  hashtpg  14438  fsumcl2lem  15684  fprodcl2lem  15906  gcdeq0  16477  lcmeq0  16560  lcmfeq0b  16590  phibndlem  16731  abvn0b  20804  cfinufil  23903  isxmet2d  24302  i1fres  25682  tdeglem4  26035  ply1domn  26099  pilem2  26430  isnsqf  27112  ppieq0  27153  chpeq0  27185  chteq0  27186  ltrnatlw  40643  bcc0  44785