Theorem necon1bd 2800

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1475   ≠ wne 2780

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 196  df-ne 2782

This theorem is referenced by:  necon4ad  2801  fvclss  6404  suppssr  7213  eceqoveq  7740  fofinf1o  8126  cantnfp1lem3  8460  cantnfp1  8461  mul0or  10546  inelr  10887  rimul  10888  rlimuni  14129  pc2dvds  15421  divsfval  16030  pleval2i  16787  lssvs0or  18931  lspsnat  18966  lmmo  20994  filssufilg  21525  hausflimi  21594  fclscf  21639  xrsmopn  22423  rectbntr0  22443  bcth3  22936  limcco  23463  ig1pdvds  23740  plyco0  23752  plypf1  23772  coeeulem  23784  coeidlem  23797  coeid3  23800  coemullem  23810  coemulhi  23814  coemulc  23815  dgradd2  23828  vieta1lem2  23870  dvtaylp  23928  musum  24717  perfectlem2  24755  dchrelbas3  24763  dchrmulid2  24777  dchreq  24783  dchrsum  24794  gausslemma2dlem4  24894  dchrisum0re  25002  coltr  25342  lmieu  25476  elspansn5  27817  atomli  28625  onsucconi  31606  poimirlem8  32587  poimirlem9  32588  poimirlem18  32597  poimirlem21  32600  poimirlem22  32601  poimirlem26  32605  lshpcmp  33293  lsator0sp  33306  atnle  33622  atlatmstc  33624  osumcllem8N  34267  osumcllem11N  34270  pexmidlem5N  34278  pexmidlem8N  34281  dochsat0  35764  dochexmidlem5  35771  dochexmidlem8  35774  congabseq  36559  perfectALTVlem2  40165