Theorem necon4bd 2976

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2957

This theorem is used by:  iftrueb  4495  om00  8567  pw2f1olem  9084  xlt2add  13371  hashfun  14562  hashtpg  14610  fsumcl2lem  15877  fprodcl2lem  16097  gcdeq0  16669  lcmeq0  16755  lcmfeq0b  16785  phibndlem  16927  abvn0b  21073  cfinufil  24227  isxmet2d  24626  i1fres  26006  tdeglem4  26358  ply1domn  26422  pilem2  26761  isnsqf  27444  ppieq0  27485  chpeq0  27517  chteq0  27518  ltrnatlw  41208  bcc0  45283