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  4494  om00  8512  pw2f1olem  9021  xlt2add  13187  hashfun  14372  hashtpg  14420  fsumcl2lem  15666  fprodcl2lem  15885  gcdeq0  16456  lcmeq0  16539  lcmfeq0b  16569  phibndlem  16709  abvn0b  20781  cfinufil  23884  isxmet2d  24283  i1fres  25674  tdeglem4  26033  ply1domn  26097  pilem2  26430  isnsqf  27113  ppieq0  27154  chpeq0  27187  chteq0  27188  ltrnatlw  40553  bcc0  44690