Theorem necon1bd 2950

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 2933	. . 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 2932

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 2933

This theorem is referenced by:  necon4ad  2951  fvclss  7232  suppssr  8192  suppssrg  8193  suppofssd  8200  eceqoveq  8834  fofinf1o  9342  cantnfp1lem3  9692  cantnfp1  9693  mul0or  11875  inelr  12228  rimul  12229  rlimuni  15564  pc2dvds  16897  divsfval  17559  pleval2i  18344  lssvs0or  21069  lspsnat  21104  psdmul  22102  lmmo  23316  filssufilg  23847  hausflimi  23916  fclscf  23961  xrsmopn  24750  rectbntr0  24770  bcth3  25281  limcco  25844  ig1pdvds  26135  plyco0  26147  plypf1  26167  coeeulem  26179  coeidlem  26192  coeid3  26195  coemullem  26205  coemulhi  26209  coemulc  26210  dgradd2  26224  vieta1lem2  26269  dvtaylp  26328  musum  27151  perfectlem2  27191  dchrelbas3  27199  dchrmullid  27213  dchreq  27219  dchrsum  27230  gausslemma2dlem4  27330  dchrisum0re  27474  muls0ord  28128  coltr  28572  lmieu  28709  pthisspthorcycl  29730  elspansn5  31501  atomli  32309  onsucconni  36401  poimirlem8  37598  poimirlem9  37599  poimirlem18  37608  poimirlem21  37611  poimirlem22  37612  poimirlem26  37616  lshpcmp  38952  lsator0sp  38965  atnle  39281  atlatmstc  39283  osumcllem8N  39928  osumcllem11N  39931  pexmidlem5N  39939  pexmidlem8N  39942  dochsat0  41422  dochexmidlem5  41429  dochexmidlem8  41432  aks6d1c4  42083  fsuppind  42560  congabseq  42945  dflim5  43300  mnringmulrcld  44200  perfectALTVlem2  47684