Theorem necon1bd 2976

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2958

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 210  df-ne 2959

This theorem is referenced by:  necon4ad  2977  fvclss  7241  suppssr  8192  suppssrg  8193  suppofssd  8200  eceqoveq  8821  fofinf1o  9290  cantnfp1lem3  9650  cantnfp1  9651  mul0or  11855  rimul  12210  rlimuni  15603  pc2dvds  16940  divsfval  17602  pleval2i  18391  lssvs0or  21215  lspsnat  21250  psdmul  22310  lmmo  23518  filssufilg  24049  hausflimi  24118  fclscf  24163  xrsmopn  24951  rectbntr0  24971  bcth3  25471  limcco  26033  ig1pdvds  26318  plyco0  26330  plypf1  26350  coeeulem  26362  coeidlem  26375  coeid3  26378  coemullem  26388  coemulhi  26392  coemulc  26393  dgradd2  26406  vieta1lem2  26453  dvtaylp  26514  musum  27336  perfectlem2  27375  dchrelbas3  27383  dchrmullid  27397  dchreq  27403  dchrsum  27414  gausslemma2dlem4  27514  dchrisum0re  27658  muls0ord  28359  coltr  28902  lmieu  29074  pthisspthorcycl  30132  elspansn5  31907  atomli  32715  onsucconni  36929  poimirlem8  38260  poimirlem9  38261  poimirlem18  38270  poimirlem21  38273  poimirlem22  38274  poimirlem26  38278  lshpcmp  39743  lsator0sp  39756  atnle  40072  atlatmstc  40074  osumcllem8N  40718  osumcllem11N  40721  pexmidlem5N  40729  pexmidlem8N  40732  dochsat0  42212  dochexmidlem5  42219  dochexmidlem8  42222  aks6d1c4  42872  sn-remul0ord  43150  fsuppind  43305  congabseq  43684  dflim5  44039  mnringmulrcld  44935  perfectALTVlem2  48470