Theorem necon1bd 2950

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1632   ≠ wne 2932

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 2933

This theorem is referenced by:  necon4ad  2951  fvclss  6664  suppssr  7496  eceqoveq  8021  fofinf1o  8408  cantnfp1lem3  8752  cantnfp1  8753  mul0or  10879  inelr  11222  rimul  11223  rlimuni  14500  pc2dvds  15805  divsfval  16429  pleval2i  17185  lssvs0or  19332  lspsnat  19367  lmmo  21406  filssufilg  21936  hausflimi  22005  fclscf  22050  xrsmopn  22836  rectbntr0  22856  bcth3  23348  limcco  23876  ig1pdvds  24155  plyco0  24167  plypf1  24187  coeeulem  24199  coeidlem  24212  coeid3  24215  coemullem  24225  coemulhi  24229  coemulc  24230  dgradd2  24243  vieta1lem2  24285  dvtaylp  24343  musum  25137  perfectlem2  25175  dchrelbas3  25183  dchrmulid2  25197  dchreq  25203  dchrsum  25214  gausslemma2dlem4  25314  dchrisum0re  25422  coltr  25762  lmieu  25896  elspansn5  28763  atomli  29571  onsucconni  32763  poimirlem8  33748  poimirlem9  33749  poimirlem18  33758  poimirlem21  33761  poimirlem22  33762  poimirlem26  33766  lshpcmp  34796  lsator0sp  34809  atnle  35125  atlatmstc  35127  osumcllem8N  35770  osumcllem11N  35773  pexmidlem5N  35781  pexmidlem8N  35784  dochsat0  37266  dochexmidlem5  37273  dochexmidlem8  37276  congabseq  38061  perfectALTVlem2  42159