Theorem necon1bd 2961

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 2944	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon1bd.1	. . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))
3	1, 2	syl5bir 242	. 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 → 𝜓))
4	3	con1d 145	1 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 = 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2943

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 206  df-ne 2944

This theorem is referenced by:  necon4ad  2962  fvclss  7115  suppssr  8012  suppssrg  8013  suppofssd  8019  eceqoveq  8611  fofinf1o  9094  cantnfp1lem3  9438  cantnfp1  9439  mul0or  11615  inelr  11963  rimul  11964  rlimuni  15259  pc2dvds  16580  divsfval  17258  pleval2i  18054  lssvs0or  20372  lspsnat  20407  lmmo  22531  filssufilg  23062  hausflimi  23131  fclscf  23176  xrsmopn  23975  rectbntr0  23995  bcth3  24495  limcco  25057  ig1pdvds  25341  plyco0  25353  plypf1  25373  coeeulem  25385  coeidlem  25398  coeid3  25401  coemullem  25411  coemulhi  25415  coemulc  25416  dgradd2  25429  vieta1lem2  25471  dvtaylp  25529  musum  26340  perfectlem2  26378  dchrelbas3  26386  dchrmulid2  26400  dchreq  26406  dchrsum  26417  gausslemma2dlem4  26517  dchrisum0re  26661  coltr  27008  lmieu  27145  elspansn5  29936  atomli  30744  pthisspthorcycl  33090  onsucconni  34626  poimirlem8  35785  poimirlem9  35786  poimirlem18  35795  poimirlem21  35798  poimirlem22  35799  poimirlem26  35803  lshpcmp  37002  lsator0sp  37015  atnle  37331  atlatmstc  37333  osumcllem8N  37977  osumcllem11N  37980  pexmidlem5N  37988  pexmidlem8N  37991  dochsat0  39471  dochexmidlem5  39478  dochexmidlem8  39481  fsuppind  40279  congabseq  40796  mnringmulrcld  41846  perfectALTVlem2  45174