Theorem necon1bd 2970

Description: Contrapositive deduction for inequality. (Contributed by NM, 21-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)

Hypothesis

Ref	Expression
necon1bd.1	⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))

Assertion

Ref	Expression
necon1bd	⊢ (𝜑 → (¬ 𝜓 → 𝐴 = 𝐵))

Proof of Theorem necon1bd

Step	Hyp	Ref	Expression
1		df-ne 2953	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon1bd.1	. . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))
3	1, 2	syl5bir 246	. 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 → 𝜓))
4	3	con1d 147	1 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 = 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2952

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 2953

This theorem is referenced by:  necon4ad  2971  fvclss  6991  suppssr  7868  suppssrg  7869  suppofssd  7875  eceqoveq  8410  fofinf1o  8822  cantnfp1lem3  9166  cantnfp1  9167  mul0or  11308  inelr  11654  rimul  11655  rlimuni  14945  pc2dvds  16260  divsfval  16868  pleval2i  17630  lssvs0or  19940  lspsnat  19975  lmmo  22070  filssufilg  22601  hausflimi  22670  fclscf  22715  xrsmopn  23503  rectbntr0  23523  bcth3  24021  limcco  24582  ig1pdvds  24866  plyco0  24878  plypf1  24898  coeeulem  24910  coeidlem  24923  coeid3  24926  coemullem  24936  coemulhi  24940  coemulc  24941  dgradd2  24954  vieta1lem2  24996  dvtaylp  25054  musum  25865  perfectlem2  25903  dchrelbas3  25911  dchrmulid2  25925  dchreq  25931  dchrsum  25942  gausslemma2dlem4  26042  dchrisum0re  26186  coltr  26530  lmieu  26667  elspansn5  29446  atomli  30254  pthisspthorcycl  32596  onsucconni  34165  poimirlem8  35335  poimirlem9  35336  poimirlem18  35345  poimirlem21  35348  poimirlem22  35349  poimirlem26  35353  lshpcmp  36554  lsator0sp  36567  atnle  36883  atlatmstc  36885  osumcllem8N  37529  osumcllem11N  37532  pexmidlem5N  37540  pexmidlem8N  37543  dochsat0  39023  dochexmidlem5  39030  dochexmidlem8  39033  fsuppind  39774  congabseq  40278  mnringmulrcld  41299  perfectALTVlem2  44597