Theorem necon1bd 2946

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2928

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 2929

This theorem is referenced by:  necon4ad  2947  fvclss  7170  suppssr  8120  suppssrg  8121  suppofssd  8128  eceqoveq  8741  fofinf1o  9211  cantnfp1lem3  9565  cantnfp1  9566  mul0or  11752  rimul  12111  rlimuni  15452  pc2dvds  16786  divsfval  17446  pleval2i  18235  lssvs0or  21042  lspsnat  21077  psdmul  22076  lmmo  23290  filssufilg  23821  hausflimi  23890  fclscf  23935  xrsmopn  24723  rectbntr0  24743  bcth3  25253  limcco  25816  ig1pdvds  26107  plyco0  26119  plypf1  26139  coeeulem  26151  coeidlem  26164  coeid3  26167  coemullem  26177  coemulhi  26181  coemulc  26182  dgradd2  26196  vieta1lem2  26241  dvtaylp  26300  musum  27123  perfectlem2  27163  dchrelbas3  27171  dchrmullid  27185  dchreq  27191  dchrsum  27202  gausslemma2dlem4  27302  dchrisum0re  27446  muls0ord  28119  coltr  28620  lmieu  28757  pthisspthorcycl  29775  elspansn5  31546  atomli  32354  onsucconni  36471  poimirlem8  37668  poimirlem9  37669  poimirlem18  37678  poimirlem21  37681  poimirlem22  37682  poimirlem26  37686  lshpcmp  39027  lsator0sp  39040  atnle  39356  atlatmstc  39358  osumcllem8N  40002  osumcllem11N  40005  pexmidlem5N  40013  pexmidlem8N  40016  dochsat0  41496  dochexmidlem5  41503  dochexmidlem8  41506  aks6d1c4  42157  sn-remul0ord  42441  fsuppind  42623  congabseq  43007  dflim5  43362  mnringmulrcld  44261  perfectALTVlem2  47753