Theorem necon1bd 2951

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  necon4ad  2952  fvclss  7197  suppssr  8147  suppssrg  8148  suppofssd  8155  eceqoveq  8771  fofinf1o  9244  cantnfp1lem3  9601  cantnfp1  9602  mul0or  11789  rimul  12148  rlimuni  15485  pc2dvds  16819  divsfval  17480  pleval2i  18269  lssvs0or  21077  lspsnat  21112  psdmul  22121  lmmo  23336  filssufilg  23867  hausflimi  23936  fclscf  23981  xrsmopn  24769  rectbntr0  24789  bcth3  25299  limcco  25862  ig1pdvds  26153  plyco0  26165  plypf1  26185  coeeulem  26197  coeidlem  26210  coeid3  26213  coemullem  26223  coemulhi  26227  coemulc  26228  dgradd2  26242  vieta1lem2  26287  dvtaylp  26346  musum  27169  perfectlem2  27209  dchrelbas3  27217  dchrmullid  27231  dchreq  27237  dchrsum  27248  gausslemma2dlem4  27348  dchrisum0re  27492  muls0ord  28193  coltr  28731  lmieu  28868  pthisspthorcycl  29887  elspansn5  31661  atomli  32469  onsucconni  36650  poimirlem8  37876  poimirlem9  37877  poimirlem18  37886  poimirlem21  37889  poimirlem22  37890  poimirlem26  37894  lshpcmp  39361  lsator0sp  39374  atnle  39690  atlatmstc  39692  osumcllem8N  40336  osumcllem11N  40339  pexmidlem5N  40347  pexmidlem8N  40350  dochsat0  41830  dochexmidlem5  41837  dochexmidlem8  41840  aks6d1c4  42491  sn-remul0ord  42775  fsuppind  42945  congabseq  43328  dflim5  43683  mnringmulrcld  44581  perfectALTVlem2  48079