Theorem necon1bd 2943

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2925

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 2926

This theorem is referenced by:  necon4ad  2944  fvclss  7181  suppssr  8135  suppssrg  8136  suppofssd  8143  eceqoveq  8756  fofinf1o  9241  cantnfp1lem3  9595  cantnfp1  9596  mul0or  11778  rimul  12137  rlimuni  15475  pc2dvds  16809  divsfval  17469  pleval2i  18258  lssvs0or  21035  lspsnat  21070  psdmul  22069  lmmo  23283  filssufilg  23814  hausflimi  23883  fclscf  23928  xrsmopn  24717  rectbntr0  24737  bcth3  25247  limcco  25810  ig1pdvds  26101  plyco0  26113  plypf1  26133  coeeulem  26145  coeidlem  26158  coeid3  26161  coemullem  26171  coemulhi  26175  coemulc  26176  dgradd2  26190  vieta1lem2  26235  dvtaylp  26294  musum  27117  perfectlem2  27157  dchrelbas3  27165  dchrmullid  27179  dchreq  27185  dchrsum  27196  gausslemma2dlem4  27296  dchrisum0re  27440  muls0ord  28111  coltr  28610  lmieu  28747  pthisspthorcycl  29765  elspansn5  31536  atomli  32344  onsucconni  36413  poimirlem8  37610  poimirlem9  37611  poimirlem18  37620  poimirlem21  37623  poimirlem22  37624  poimirlem26  37628  lshpcmp  38969  lsator0sp  38982  atnle  39298  atlatmstc  39300  osumcllem8N  39945  osumcllem11N  39948  pexmidlem5N  39956  pexmidlem8N  39959  dochsat0  41439  dochexmidlem5  41446  dochexmidlem8  41449  aks6d1c4  42100  sn-remul0ord  42384  fsuppind  42566  congabseq  42950  dflim5  43305  mnringmulrcld  44204  perfectALTVlem2  47710