Theorem necon1bd 2982

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1567   ≠ wne 2964

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 2965

This theorem is referenced by:  necon4ad  2983  fvclss  7237  suppssr  8187  suppssrg  8188  suppofssd  8195  eceqoveq  8816  fofinf1o  9285  cantnfp1lem3  9645  cantnfp1  9646  mul0or  11850  rimul  12205  rlimuni  15597  pc2dvds  16935  divsfval  17597  pleval2i  18386  lssvs0or  21208  lspsnat  21243  psdmul  22294  lmmo  23502  filssufilg  24033  hausflimi  24102  fclscf  24147  xrsmopn  24935  rectbntr0  24955  bcth3  25455  limcco  26017  ig1pdvds  26302  plyco0  26314  plypf1  26334  coeeulem  26346  coeidlem  26359  coeid3  26362  coemullem  26372  coemulhi  26376  coemulc  26377  dgradd2  26390  vieta1lem2  26437  dvtaylp  26495  musum  27317  perfectlem2  27356  dchrelbas3  27364  dchrmullid  27378  dchreq  27384  dchrsum  27395  gausslemma2dlem4  27495  dchrisum0re  27639  muls0ord  28340  coltr  28879  lmieu  29047  pthisspthorcycl  30088  elspansn5  31863  atomli  32671  onsucconni  36833  poimirlem8  38162  poimirlem9  38163  poimirlem18  38172  poimirlem21  38175  poimirlem22  38176  poimirlem26  38180  lshpcmp  39647  lsator0sp  39660  atnle  39976  atlatmstc  39978  osumcllem8N  40622  osumcllem11N  40625  pexmidlem5N  40633  pexmidlem8N  40636  dochsat0  42116  dochexmidlem5  42123  dochexmidlem8  42126  aks6d1c4  42776  sn-remul0ord  43052  fsuppind  43207  congabseq  43586  dflim5  43941  mnringmulrcld  44837  perfectALTVlem2  48369