Theorem necon1bd 3005

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 2988	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon1bd.1	. . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))
3	1, 2	syl5bir 246	. 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 → 𝜓))
4	3	con1d 147	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:  necon4ad  3006  fvclss  6979  suppssr  7844  suppofssd  7850  eceqoveq  8385  fofinf1o  8783  cantnfp1lem3  9127  cantnfp1  9128  mul0or  11269  inelr  11615  rimul  11616  rlimuni  14899  pc2dvds  16205  divsfval  16812  pleval2i  17566  lssvs0or  19875  lspsnat  19910  lmmo  21985  filssufilg  22516  hausflimi  22585  fclscf  22630  xrsmopn  23417  rectbntr0  23437  bcth3  23935  limcco  24496  ig1pdvds  24777  plyco0  24789  plypf1  24809  coeeulem  24821  coeidlem  24834  coeid3  24837  coemullem  24847  coemulhi  24851  coemulc  24852  dgradd2  24865  vieta1lem2  24907  dvtaylp  24965  musum  25776  perfectlem2  25814  dchrelbas3  25822  dchrmulid2  25836  dchreq  25842  dchrsum  25853  gausslemma2dlem4  25953  dchrisum0re  26097  coltr  26441  lmieu  26578  elspansn5  29357  atomli  30165  pthisspthorcycl  32488  onsucconni  33898  poimirlem8  35065  poimirlem9  35066  poimirlem18  35075  poimirlem21  35078  poimirlem22  35079  poimirlem26  35083  lshpcmp  36284  lsator0sp  36297  atnle  36613  atlatmstc  36615  osumcllem8N  37259  osumcllem11N  37262  pexmidlem5N  37270  pexmidlem8N  37273  dochsat0  38753  dochexmidlem5  38760  dochexmidlem8  38763  fsuppind  39456  congabseq  39915  mnringmulrcld  40936  perfectALTVlem2  44240