Theorem necon1bd 2952

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1547   ≠ wne 2934

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 208  df-ne 2935

This theorem is referenced by:  necon4ad  2953  fvclss  7185  suppssr  8135  suppssrg  8136  suppofssd  8143  eceqoveq  8759  fofinf1o  9232  cantnfp1lem3  9592  cantnfp1  9593  mul0or  11781  rimul  12141  rlimuni  15503  pc2dvds  16841  divsfval  17502  pleval2i  18291  lssvs0or  21103  lspsnat  21138  psdmul  22154  lmmo  23363  filssufilg  23894  hausflimi  23963  fclscf  24008  xrsmopn  24796  rectbntr0  24816  bcth3  25316  limcco  25878  ig1pdvds  26163  plyco0  26175  plypf1  26195  coeeulem  26207  coeidlem  26220  coeid3  26223  coemullem  26233  coemulhi  26237  coemulc  26238  dgradd2  26251  vieta1lem2  26295  dvtaylp  26353  musum  27172  perfectlem2  27211  dchrelbas3  27219  dchrmullid  27233  dchreq  27239  dchrsum  27250  gausslemma2dlem4  27350  dchrisum0re  27494  muls0ord  28195  coltr  28733  lmieu  28870  pthisspthorcycl  29888  elspansn5  31663  atomli  32471  onsucconni  36665  poimirlem8  37995  poimirlem9  37996  poimirlem18  38005  poimirlem21  38008  poimirlem22  38009  poimirlem26  38013  lshpcmp  39480  lsator0sp  39493  atnle  39809  atlatmstc  39811  osumcllem8N  40455  osumcllem11N  40458  pexmidlem5N  40466  pexmidlem8N  40469  dochsat0  41949  dochexmidlem5  41956  dochexmidlem8  41959  aks6d1c4  42609  sn-remul0ord  42885  fsuppind  43040  congabseq  43419  dflim5  43774  mnringmulrcld  44672  perfectALTVlem2  48213