Theorem necon1bd 3017

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 3000	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon1bd.1	. . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))
3	1, 2	syl5bir 235	. 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 → 𝜓))
4	3	con1d 142	1 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 = 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1658   ≠ wne 2999

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 199  df-ne 3000

This theorem is referenced by:  necon4ad  3018  fvclss  6755  suppssr  7591  eceqoveq  8118  fofinf1o  8510  cantnfp1lem3  8854  cantnfp1  8855  mul0or  10992  inelr  11340  rimul  11341  rlimuni  14658  pc2dvds  15954  divsfval  16560  pleval2i  17317  lssvs0or  19469  lspsnat  19505  lmmo  21555  filssufilg  22085  hausflimi  22154  fclscf  22199  xrsmopn  22985  rectbntr0  23005  bcth3  23499  limcco  24056  ig1pdvds  24335  plyco0  24347  plypf1  24367  coeeulem  24379  coeidlem  24392  coeid3  24395  coemullem  24405  coemulhi  24409  coemulc  24410  dgradd2  24423  vieta1lem2  24465  dvtaylp  24523  musum  25330  perfectlem2  25368  dchrelbas3  25376  dchrmulid2  25390  dchreq  25396  dchrsum  25407  gausslemma2dlem4  25507  dchrisum0re  25615  coltr  25959  lmieu  26093  elspansn5  28988  atomli  29796  onsucconni  32969  poimirlem8  33961  poimirlem9  33962  poimirlem18  33971  poimirlem21  33974  poimirlem22  33975  poimirlem26  33979  lshpcmp  35063  lsator0sp  35076  atnle  35392  atlatmstc  35394  osumcllem8N  36038  osumcllem11N  36041  pexmidlem5N  36049  pexmidlem8N  36052  dochsat0  37532  dochexmidlem5  37539  dochexmidlem8  37542  congabseq  38384  perfectALTVlem2  42461