Theorem necon1bd 2973

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 2956	. . 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 2955

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 2956

This theorem is used by:  necon4ad  2974  fvclss  7238  suppssr  8193  suppssrg  8194  suppofssd  8201  eceqoveq  8822  fofinf1o  9299  cantnfp1lem3  9659  cantnfp1  9660  mul0or  11878  rimul  12233  rlimuni  15637  pc2dvds  16971  divsfval  17633  pleval2i  18422  lssvs0or  21297  lspsnat  21332  psdmul  22394  lmmo  23605  filssufilg  24137  hausflimi  24206  fclscf  24251  xrsmopn  25039  rectbntr0  25059  bcth3  25559  limcco  26120  ig1pdvds  26405  plyco0  26417  plypf1  26438  coeeulem  26450  coeidlem  26463  coeid3  26466  coemullem  26476  coemulhi  26480  coemulc  26481  dgradd2  26494  vieta1lem2  26543  dvtaylp  26606  musum  27427  perfectlem2  27466  dchrelbas3  27474  dchrmullid  27488  dchreq  27494  dchrsum  27505  gausslemma2dlem4  27605  dchrisum0re  27749  muls0ord  28450  coltr  28995  lmieu  29168  pthisspthorcycl  30269  elspansn5  32055  atomli  32863  onsucconni  37056  poimirlem8  38377  poimirlem9  38378  poimirlem18  38387  poimirlem21  38390  poimirlem22  38391  poimirlem26  38395  lshpcmp  39861  lsator0sp  39874  atnle  40190  atlatmstc  40192  osumcllem8N  40836  osumcllem11N  40839  pexmidlem5N  40847  pexmidlem8N  40850  dochsat0  42330  dochexmidlem5  42337  dochexmidlem8  42340  aks6d1c4  42990  sn-remul0ord  43283  fsuppind  43436  congabseq  43815  dflim5  44170  mnringmulrcld  45066  perfectALTVlem2  48638