Theorem necon1bd 3034

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 3017	. . 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 3016

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 3017

This theorem is referenced by:  necon4ad  3035  fvclss  7001  suppssr  7861  suppofssd  7867  eceqoveq  8402  fofinf1o  8799  cantnfp1lem3  9143  cantnfp1  9144  mul0or  11280  inelr  11628  rimul  11629  rlimuni  14907  pc2dvds  16215  divsfval  16820  pleval2i  17574  lssvs0or  19882  lspsnat  19917  lmmo  21988  filssufilg  22519  hausflimi  22588  fclscf  22633  xrsmopn  23420  rectbntr0  23440  bcth3  23934  limcco  24491  ig1pdvds  24770  plyco0  24782  plypf1  24802  coeeulem  24814  coeidlem  24827  coeid3  24830  coemullem  24840  coemulhi  24844  coemulc  24845  dgradd2  24858  vieta1lem2  24900  dvtaylp  24958  musum  25768  perfectlem2  25806  dchrelbas3  25814  dchrmulid2  25828  dchreq  25834  dchrsum  25845  gausslemma2dlem4  25945  dchrisum0re  26089  coltr  26433  lmieu  26570  elspansn5  29351  atomli  30159  pthisspthorcycl  32375  onsucconni  33785  poimirlem8  34915  poimirlem9  34916  poimirlem18  34925  poimirlem21  34928  poimirlem22  34929  poimirlem26  34933  lshpcmp  36139  lsator0sp  36152  atnle  36468  atlatmstc  36470  osumcllem8N  37114  osumcllem11N  37117  pexmidlem5N  37125  pexmidlem8N  37128  dochsat0  38608  dochexmidlem5  38615  dochexmidlem8  38618  congabseq  39591  perfectALTVlem2  43907