Theorem necon1bd 2978

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

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 2961

This theorem is used by:  necon4ad  2979  fvclss  7241  suppssr  8193  suppssrg  8194  suppofssd  8201  eceqoveq  8822  fofinf1o  9292  cantnfp1lem3  9652  cantnfp1  9653  mul0or  11865  rimul  12220  rlimuni  15620  pc2dvds  16956  divsfval  17618  pleval2i  18407  lssvs0or  21263  lspsnat  21298  psdmul  22358  lmmo  23566  filssufilg  24097  hausflimi  24166  fclscf  24211  xrsmopn  24999  rectbntr0  25019  bcth3  25519  limcco  26081  ig1pdvds  26366  plyco0  26378  plypf1  26398  coeeulem  26410  coeidlem  26423  coeid3  26426  coemullem  26436  coemulhi  26440  coemulc  26441  dgradd2  26454  vieta1lem2  26501  dvtaylp  26562  musum  27384  perfectlem2  27423  dchrelbas3  27431  dchrmullid  27445  dchreq  27451  dchrsum  27462  gausslemma2dlem4  27562  dchrisum0re  27706  muls0ord  28407  coltr  28950  lmieu  29122  pthisspthorcycl  30180  elspansn5  31955  atomli  32763  onsucconni  36981  poimirlem8  38312  poimirlem9  38313  poimirlem18  38322  poimirlem21  38325  poimirlem22  38326  poimirlem26  38330  lshpcmp  39795  lsator0sp  39808  atnle  40124  atlatmstc  40126  osumcllem8N  40770  osumcllem11N  40773  pexmidlem5N  40781  pexmidlem8N  40784  dochsat0  42264  dochexmidlem5  42271  dochexmidlem8  42274  aks6d1c4  42924  sn-remul0ord  43202  fsuppind  43355  congabseq  43734  dflim5  44089  mnringmulrcld  44985  perfectALTVlem2  48520