Theorem necon1bd 2960

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 2943	. . 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 2942

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 2943

This theorem is referenced by:  necon4ad  2961  fvclss  7097  suppssr  7983  suppssrg  7984  suppofssd  7990  eceqoveq  8569  fofinf1o  9024  cantnfp1lem3  9368  cantnfp1  9369  mul0or  11545  inelr  11893  rimul  11894  rlimuni  15187  pc2dvds  16508  divsfval  17175  pleval2i  17969  lssvs0or  20287  lspsnat  20322  lmmo  22439  filssufilg  22970  hausflimi  23039  fclscf  23084  xrsmopn  23881  rectbntr0  23901  bcth3  24400  limcco  24962  ig1pdvds  25246  plyco0  25258  plypf1  25278  coeeulem  25290  coeidlem  25303  coeid3  25306  coemullem  25316  coemulhi  25320  coemulc  25321  dgradd2  25334  vieta1lem2  25376  dvtaylp  25434  musum  26245  perfectlem2  26283  dchrelbas3  26291  dchrmulid2  26305  dchreq  26311  dchrsum  26322  gausslemma2dlem4  26422  dchrisum0re  26566  coltr  26912  lmieu  27049  elspansn5  29837  atomli  30645  pthisspthorcycl  32990  onsucconni  34553  poimirlem8  35712  poimirlem9  35713  poimirlem18  35722  poimirlem21  35725  poimirlem22  35726  poimirlem26  35730  lshpcmp  36929  lsator0sp  36942  atnle  37258  atlatmstc  37260  osumcllem8N  37904  osumcllem11N  37907  pexmidlem5N  37915  pexmidlem8N  37918  dochsat0  39398  dochexmidlem5  39405  dochexmidlem8  39408  fsuppind  40202  congabseq  40712  mnringmulrcld  41735  perfectALTVlem2  45062