Theorem necon4bd 2981

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

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

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 2962

This theorem is used by:  iftrueb  4505  om00  8569  pw2f1olem  9079  xlt2add  13304  hashfun  14494  hashtpg  14542  fsumcl2lem  15808  fprodcl2lem  16030  gcdeq0  16600  lcmeq0  16683  lcmfeq0b  16713  phibndlem  16854  abvn0b  20976  cfinufil  24122  isxmet2d  24521  i1fres  25901  tdeglem4  26254  ply1domn  26318  pilem2  26652  isnsqf  27336  ppieq0  27377  chpeq0  27409  chteq0  27410  ltrnatlw  40998  bcc0  45091