Theorem necon1bd 2977

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 2960	. . 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 2959

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 2960

This theorem is used by:  necon4ad  2978  fvclss  7276  suppssr  8250  suppssrg  8251  suppofssd  8258  eceqoveq  8881  fofinf1o  9359  cantnfp1lem3  9718  cantnfp1  9719  mul0or  11996  rimul  12351  rlimuni  15761  pc2dvds  17101  divsfval  17769  pleval2i  18558  lssvs0or  21439  lspsnat  21474  psdmul  22542  lmmo  23753  filssufilg  24285  hausflimi  24354  fclscf  24399  xrsmopn  25187  rectbntr0  25207  bcth3  25707  limcco  26268  ig1pdvds  26553  plyco0  26565  plypf1  26586  coeeulem  26598  coeidlem  26611  coeid3  26614  coemullem  26624  coemulhi  26628  coemulc  26629  dgradd2  26642  vieta1lem2  26689  dvtaylp  26754  musum  27575  perfectlem2  27614  dchrelbas3  27622  dchrmullid  27636  dchreq  27642  dchrsum  27653  gausslemma2dlem4  27753  dchrisum0re  27897  muls0ord  28628  coltr  29173  lmieu  29346  pthisspthorcycl  30447  elspansn5  32233  atomli  33041  onsucconni  37440  poimirlem8  38814  poimirlem9  38815  poimirlem18  38824  poimirlem21  38827  poimirlem22  38828  poimirlem26  38832  lshpcmp  40311  lsator0sp  40324  atnle  40640  atlatmstc  40642  osumcllem8N  41286  osumcllem11N  41289  pexmidlem5N  41297  pexmidlem8N  41300  dochsat0  42780  dochexmidlem5  42787  dochexmidlem8  42790  aks6d1c4  43440  sn-remul0ord  43725  fsuppind  43884  congabseq  44247  dflim5  44592  mnringmulrcld  45487  perfectALTVlem2  49093