Theorem necon4bd 3007

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538   ≠ wne 2987

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 210  df-ne 2988

This theorem is referenced by:  om00  8184  pw2f1olem  8604  xlt2add  12641  hashfun  13794  hashtpg  13839  fsumcl2lem  15080  fprodcl2lem  15296  gcdeq0  15855  lcmeq0  15934  lcmfeq0b  15964  phibndlem  16097  abvn0b  20068  cfinufil  22533  isxmet2d  22934  i1fres  24309  tdeglem4  24661  ply1domn  24724  pilem2  25047  isnsqf  25720  ppieq0  25761  chpeq0  25792  chteq0  25793  ltrnatlw  37479  bcc0  41044