Theorem necon1bd 2956

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 2939	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon1bd.1	. . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))
3	1, 2	biimtrrid 242	. 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 → 𝜓))
4	3	con1d 145	1 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 = 𝐵))

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

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 206  df-ne 2939

This theorem is referenced by:  necon4ad  2957  fvclss  7242  suppssr  8183  suppssrg  8184  suppofssd  8190  eceqoveq  8818  fofinf1o  9329  cantnfp1lem3  9677  cantnfp1  9678  mul0or  11858  inelr  12206  rimul  12207  rlimuni  15498  pc2dvds  16816  divsfval  17497  pleval2i  18293  lssvs0or  20868  lspsnat  20903  lmmo  23104  filssufilg  23635  hausflimi  23704  fclscf  23749  xrsmopn  24548  rectbntr0  24568  bcth3  25079  limcco  25642  ig1pdvds  25929  plyco0  25941  plypf1  25961  coeeulem  25973  coeidlem  25986  coeid3  25989  coemullem  25999  coemulhi  26003  coemulc  26004  dgradd2  26018  vieta1lem2  26060  dvtaylp  26118  musum  26931  perfectlem2  26969  dchrelbas3  26977  dchrmullid  26991  dchreq  26997  dchrsum  27008  gausslemma2dlem4  27108  dchrisum0re  27252  coltr  28165  lmieu  28302  elspansn5  31094  atomli  31902  pthisspthorcycl  34417  onsucconni  35625  poimirlem8  36799  poimirlem9  36800  poimirlem18  36809  poimirlem21  36812  poimirlem22  36813  poimirlem26  36817  lshpcmp  38161  lsator0sp  38174  atnle  38490  atlatmstc  38492  osumcllem8N  39137  osumcllem11N  39140  pexmidlem5N  39148  pexmidlem8N  39151  dochsat0  40631  dochexmidlem5  40638  dochexmidlem8  40641  fsuppind  41464  congabseq  42015  dflim5  42381  mnringmulrcld  43289  perfectALTVlem2  46688