Theorem necon1bd 2958

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2940

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 207  df-ne 2941

This theorem is referenced by:  necon4ad  2959  fvclss  7261  suppssr  8220  suppssrg  8221  suppofssd  8228  eceqoveq  8862  fofinf1o  9372  cantnfp1lem3  9720  cantnfp1  9721  mul0or  11903  inelr  12256  rimul  12257  rlimuni  15586  pc2dvds  16917  divsfval  17592  pleval2i  18381  lssvs0or  21112  lspsnat  21147  psdmul  22170  lmmo  23388  filssufilg  23919  hausflimi  23988  fclscf  24033  xrsmopn  24834  rectbntr0  24854  bcth3  25365  limcco  25928  ig1pdvds  26219  plyco0  26231  plypf1  26251  coeeulem  26263  coeidlem  26276  coeid3  26279  coemullem  26289  coemulhi  26293  coemulc  26294  dgradd2  26308  vieta1lem2  26353  dvtaylp  26412  musum  27234  perfectlem2  27274  dchrelbas3  27282  dchrmullid  27296  dchreq  27302  dchrsum  27313  gausslemma2dlem4  27413  dchrisum0re  27557  muls0ord  28211  coltr  28655  lmieu  28792  pthisspthorcycl  29822  elspansn5  31593  atomli  32401  onsucconni  36438  poimirlem8  37635  poimirlem9  37636  poimirlem18  37645  poimirlem21  37648  poimirlem22  37649  poimirlem26  37653  lshpcmp  38989  lsator0sp  39002  atnle  39318  atlatmstc  39320  osumcllem8N  39965  osumcllem11N  39968  pexmidlem5N  39976  pexmidlem8N  39979  dochsat0  41459  dochexmidlem5  41466  dochexmidlem8  41469  aks6d1c4  42125  fsuppind  42600  congabseq  42986  dflim5  43342  mnringmulrcld  44247  perfectALTVlem2  47709