Theorem necon4bd 3035

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1536   ≠ wne 3015

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 209  df-ne 3016

This theorem is referenced by:  om00  8194  pw2f1olem  8614  xlt2add  12647  hashfun  13795  hashtpg  13840  fsumcl2lem  15083  fprodcl2lem  15299  gcdeq0  15860  lcmeq0  15939  lcmfeq0b  15969  phibndlem  16102  abvn0b  20070  cfinufil  22531  isxmet2d  22932  i1fres  24301  tdeglem4  24652  ply1domn  24715  pilem2  25038  isnsqf  25710  ppieq0  25751  chpeq0  25782  chteq0  25783  ltrnatlw  37352  bcc0  40746