Theorem necon1bd 2841

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1523   ≠ wne 2823

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 197  df-ne 2824

This theorem is referenced by:  necon4ad  2842  fvclss  6540  suppssr  7371  eceqoveq  7895  fofinf1o  8282  cantnfp1lem3  8615  cantnfp1  8616  mul0or  10705  inelr  11048  rimul  11049  rlimuni  14325  pc2dvds  15630  divsfval  16254  pleval2i  17011  lssvs0or  19158  lspsnat  19193  lmmo  21232  filssufilg  21762  hausflimi  21831  fclscf  21876  xrsmopn  22662  rectbntr0  22682  bcth3  23174  limcco  23702  ig1pdvds  23981  plyco0  23993  plypf1  24013  coeeulem  24025  coeidlem  24038  coeid3  24041  coemullem  24051  coemulhi  24055  coemulc  24056  dgradd2  24069  vieta1lem2  24111  dvtaylp  24169  musum  24962  perfectlem2  25000  dchrelbas3  25008  dchrmulid2  25022  dchreq  25028  dchrsum  25039  gausslemma2dlem4  25139  dchrisum0re  25247  coltr  25587  lmieu  25721  elspansn5  28561  atomli  29369  onsucconni  32561  poimirlem8  33547  poimirlem9  33548  poimirlem18  33557  poimirlem21  33560  poimirlem22  33561  poimirlem26  33565  lshpcmp  34593  lsator0sp  34606  atnle  34922  atlatmstc  34924  osumcllem8N  35567  osumcllem11N  35570  pexmidlem5N  35578  pexmidlem8N  35581  dochsat0  37063  dochexmidlem5  37070  dochexmidlem8  37073  congabseq  37858  perfectALTVlem2  41956