Theorem necon1bd 2943

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 2926	. . 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 2925

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 2926

This theorem is referenced by:  necon4ad  2944  fvclss  7215  suppssr  8174  suppssrg  8175  suppofssd  8182  eceqoveq  8795  fofinf1o  9283  cantnfp1lem3  9633  cantnfp1  9634  mul0or  11818  rimul  12177  rlimuni  15516  pc2dvds  16850  divsfval  17510  pleval2i  18295  lssvs0or  21020  lspsnat  21055  psdmul  22053  lmmo  23267  filssufilg  23798  hausflimi  23867  fclscf  23912  xrsmopn  24701  rectbntr0  24721  bcth3  25231  limcco  25794  ig1pdvds  26085  plyco0  26097  plypf1  26117  coeeulem  26129  coeidlem  26142  coeid3  26145  coemullem  26155  coemulhi  26159  coemulc  26160  dgradd2  26174  vieta1lem2  26219  dvtaylp  26278  musum  27101  perfectlem2  27141  dchrelbas3  27149  dchrmullid  27163  dchreq  27169  dchrsum  27180  gausslemma2dlem4  27280  dchrisum0re  27424  muls0ord  28088  coltr  28574  lmieu  28711  pthisspthorcycl  29732  elspansn5  31503  atomli  32311  onsucconni  36425  poimirlem8  37622  poimirlem9  37623  poimirlem18  37632  poimirlem21  37635  poimirlem22  37636  poimirlem26  37640  lshpcmp  38981  lsator0sp  38994  atnle  39310  atlatmstc  39312  osumcllem8N  39957  osumcllem11N  39960  pexmidlem5N  39968  pexmidlem8N  39971  dochsat0  41451  dochexmidlem5  41458  dochexmidlem8  41461  aks6d1c4  42112  sn-remul0ord  42396  fsuppind  42578  congabseq  42963  dflim5  43318  mnringmulrcld  44217  perfectALTVlem2  47723