Theorem necon1bd 2947

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2929

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 207  df-ne 2930

This theorem is referenced by:  necon4ad  2948  fvclss  7184  suppssr  8134  suppssrg  8135  suppofssd  8142  eceqoveq  8755  fofinf1o  9227  cantnfp1lem3  9581  cantnfp1  9582  mul0or  11768  rimul  12127  rlimuni  15464  pc2dvds  16798  divsfval  17459  pleval2i  18248  lssvs0or  21056  lspsnat  21091  psdmul  22100  lmmo  23315  filssufilg  23846  hausflimi  23915  fclscf  23960  xrsmopn  24748  rectbntr0  24768  bcth3  25278  limcco  25841  ig1pdvds  26132  plyco0  26144  plypf1  26164  coeeulem  26176  coeidlem  26189  coeid3  26192  coemullem  26202  coemulhi  26206  coemulc  26207  dgradd2  26221  vieta1lem2  26266  dvtaylp  26325  musum  27148  perfectlem2  27188  dchrelbas3  27196  dchrmullid  27210  dchreq  27216  dchrsum  27227  gausslemma2dlem4  27327  dchrisum0re  27471  muls0ord  28144  coltr  28645  lmieu  28782  pthisspthorcycl  29801  elspansn5  31575  atomli  32383  onsucconni  36553  poimirlem8  37741  poimirlem9  37742  poimirlem18  37751  poimirlem21  37754  poimirlem22  37755  poimirlem26  37759  lshpcmp  39160  lsator0sp  39173  atnle  39489  atlatmstc  39491  osumcllem8N  40135  osumcllem11N  40138  pexmidlem5N  40146  pexmidlem8N  40149  dochsat0  41629  dochexmidlem5  41636  dochexmidlem8  41639  aks6d1c4  42290  sn-remul0ord  42578  fsuppind  42748  congabseq  43131  dflim5  43486  mnringmulrcld  44385  perfectALTVlem2  47884