Theorem necon1bd 2973

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 2956	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon1bd.1	. . 3 ⊢ (𝜑 → (𝐴 ≠ 𝐵 → 𝜓))
3	1, 2	biimtrrid 246	. 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 → 𝜓))
4	3	con1d 146	1 ⊢ (𝜑 → (¬ 𝜓 → 𝐴 = 𝐵))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1569   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2956

This theorem is used by:  necon4ad  2974  fvclss  7246  suppssr  8216  suppssrg  8217  suppofssd  8224  eceqoveq  8847  fofinf1o  9325  cantnfp1lem3  9685  cantnfp1  9686  mul0or  11960  rimul  12315  rlimuni  15723  pc2dvds  17063  divsfval  17725  pleval2i  18514  lssvs0or  21394  lspsnat  21429  psdmul  22493  lmmo  23704  filssufilg  24236  hausflimi  24305  fclscf  24350  xrsmopn  25138  rectbntr0  25158  bcth3  25658  limcco  26219  ig1pdvds  26504  plyco0  26516  plypf1  26537  coeeulem  26549  coeidlem  26562  coeid3  26565  coemullem  26575  coemulhi  26579  coemulc  26580  dgradd2  26593  vieta1lem2  26640  dvtaylp  26703  musum  27524  perfectlem2  27563  dchrelbas3  27571  dchrmullid  27585  dchreq  27591  dchrsum  27602  gausslemma2dlem4  27702  dchrisum0re  27846  muls0ord  28577  coltr  29122  lmieu  29295  pthisspthorcycl  30396  elspansn5  32182  atomli  32990  onsucconni  37318  poimirlem8  38640  poimirlem9  38641  poimirlem18  38650  poimirlem21  38653  poimirlem22  38654  poimirlem26  38658  lshpcmp  40139  lsator0sp  40152  atnle  40468  atlatmstc  40470  osumcllem8N  41114  osumcllem11N  41117  pexmidlem5N  41125  pexmidlem8N  41128  dochsat0  42608  dochexmidlem5  42615  dochexmidlem8  42618  aks6d1c4  43268  sn-remul0ord  43553  fsuppind  43712  congabseq  44075  dflim5  44425  mnringmulrcld  45320  perfectALTVlem2  48914