Theorem necon4bd 2948

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2928

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 2929

This theorem is referenced by:  iftrueb  4485  om00  8490  pw2f1olem  8994  xlt2add  13159  hashfun  14344  hashtpg  14392  fsumcl2lem  15638  fprodcl2lem  15857  gcdeq0  16428  lcmeq0  16511  lcmfeq0b  16541  phibndlem  16681  abvn0b  20751  cfinufil  23843  isxmet2d  24242  i1fres  25633  tdeglem4  25992  ply1domn  26056  pilem2  26389  isnsqf  27072  ppieq0  27113  chpeq0  27146  chteq0  27147  ltrnatlw  40281  bcc0  44432