Theorem necon1bd 3036

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 3018

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 209  df-ne 3019

This theorem is referenced by:  necon4ad  3037  fvclss  7003  suppssr  7863  suppofssd  7869  eceqoveq  8404  fofinf1o  8801  cantnfp1lem3  9145  cantnfp1  9146  mul0or  11282  inelr  11630  rimul  11631  rlimuni  14909  pc2dvds  16217  divsfval  16822  pleval2i  17576  lssvs0or  19884  lspsnat  19919  lmmo  21990  filssufilg  22521  hausflimi  22590  fclscf  22635  xrsmopn  23422  rectbntr0  23442  bcth3  23936  limcco  24493  ig1pdvds  24772  plyco0  24784  plypf1  24804  coeeulem  24816  coeidlem  24829  coeid3  24832  coemullem  24842  coemulhi  24846  coemulc  24847  dgradd2  24860  vieta1lem2  24902  dvtaylp  24960  musum  25770  perfectlem2  25808  dchrelbas3  25816  dchrmulid2  25830  dchreq  25836  dchrsum  25847  gausslemma2dlem4  25947  dchrisum0re  26091  coltr  26435  lmieu  26572  elspansn5  29353  atomli  30161  pthisspthorcycl  32377  onsucconni  33787  poimirlem8  34902  poimirlem9  34903  poimirlem18  34912  poimirlem21  34915  poimirlem22  34916  poimirlem26  34920  lshpcmp  36126  lsator0sp  36139  atnle  36455  atlatmstc  36457  osumcllem8N  37101  osumcllem11N  37104  pexmidlem5N  37112  pexmidlem8N  37115  dochsat0  38595  dochexmidlem5  38602  dochexmidlem8  38605  congabseq  39578  perfectALTVlem2  43894