Theorem necon4bd 2979

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

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

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 2960

This theorem is used by:  iftrueb  4498  om00  8611  pw2f1olem  9128  xlt2add  13417  hashfun  14609  hashtpg  14657  fsumcl2lem  15926  fprodcl2lem  16146  gcdeq0  16718  lcmeq0  16804  lcmfeq0b  16834  phibndlem  16976  abvn0b  21123  cfinufil  24277  isxmet2d  24676  i1fres  26056  tdeglem4  26408  ply1domn  26472  pilem2  26809  isnsqf  27492  ppieq0  27533  chpeq0  27565  chteq0  27566  ltrnatlw  41432  bcc0  45516