Theorem necon1bd 2974

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2957

This theorem is used by:  necon4ad  2975  fvclss  7243  suppssr  8205  suppssrg  8206  suppofssd  8213  eceqoveq  8836  fofinf1o  9314  cantnfp1lem3  9674  cantnfp1  9675  mul0or  11949  rimul  12304  rlimuni  15710  pc2dvds  17050  divsfval  17712  pleval2i  18501  lssvs0or  21381  lspsnat  21416  psdmul  22480  lmmo  23691  filssufilg  24223  hausflimi  24292  fclscf  24337  xrsmopn  25125  rectbntr0  25145  bcth3  25645  limcco  26206  ig1pdvds  26491  plyco0  26503  plypf1  26524  coeeulem  26536  coeidlem  26549  coeid3  26552  coemullem  26562  coemulhi  26566  coemulc  26567  dgradd2  26580  vieta1lem2  26627  dvtaylp  26690  musum  27511  perfectlem2  27550  dchrelbas3  27558  dchrmullid  27572  dchreq  27578  dchrsum  27589  gausslemma2dlem4  27689  dchrisum0re  27833  muls0ord  28564  coltr  29109  lmieu  29282  pthisspthorcycl  30383  elspansn5  32169  atomli  32977  onsucconni  37205  poimirlem8  38526  poimirlem9  38527  poimirlem18  38536  poimirlem21  38539  poimirlem22  38540  poimirlem26  38544  lshpcmp  40025  lsator0sp  40038  atnle  40354  atlatmstc  40356  osumcllem8N  41000  osumcllem11N  41003  pexmidlem5N  41011  pexmidlem8N  41014  dochsat0  42494  dochexmidlem5  42501  dochexmidlem8  42504  aks6d1c4  43154  sn-remul0ord  43439  fsuppind  43598  congabseq  43960  dflim5  44315  mnringmulrcld  45211  perfectALTVlem2  48789