Theorem necon1bd 2799

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1474   ≠ wne 2779

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 195  df-ne 2781

This theorem is referenced by:  necon4ad  2800  fvclss  6382  suppssr  7190  eceqoveq  7717  fofinf1o  8103  cantnfp1lem3  8437  cantnfp1  8438  mul0or  10516  inelr  10857  rimul  10858  rlimuni  14075  pc2dvds  15367  divsfval  15976  pleval2i  16733  lssvs0or  18877  lspsnat  18912  lmmo  20936  filssufilg  21467  hausflimi  21536  fclscf  21581  xrsmopn  22355  rectbntr0  22375  bcth3  22853  limcco  23380  ig1pdvds  23657  plyco0  23669  plypf1  23689  coeeulem  23701  coeidlem  23714  coeid3  23717  coemullem  23727  coemulhi  23731  coemulc  23732  dgradd2  23745  vieta1lem2  23787  dvtaylp  23845  musum  24634  perfectlem2  24672  dchrelbas3  24680  dchrmulid2  24694  dchreq  24700  dchrsum  24711  gausslemma2dlem4  24811  dchrisum0re  24919  coltr  25260  lmieu  25394  elspansn5  27623  atomli  28431  onsucconi  31412  poimirlem8  32390  poimirlem9  32391  poimirlem18  32400  poimirlem21  32403  poimirlem22  32404  poimirlem26  32408  lshpcmp  33096  lsator0sp  33109  atnle  33425  atlatmstc  33427  osumcllem8N  34070  osumcllem11N  34073  pexmidlem5N  34081  pexmidlem8N  34084  dochsat0  35567  dochexmidlem5  35574  dochexmidlem8  35577  congabseq  36362  perfectALTVlem2  39970