Theorem necon1bd 2957

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

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

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 206  df-ne 2940

This theorem is referenced by:  necon4ad  2958  fvclss  7243  suppssr  8185  suppssrg  8186  suppofssd  8192  eceqoveq  8820  fofinf1o  9331  cantnfp1lem3  9679  cantnfp1  9680  mul0or  11859  inelr  12207  rimul  12208  rlimuni  15499  pc2dvds  16817  divsfval  17498  pleval2i  18294  lssvs0or  20869  lspsnat  20904  lmmo  23105  filssufilg  23636  hausflimi  23705  fclscf  23750  xrsmopn  24549  rectbntr0  24569  bcth3  25080  limcco  25643  ig1pdvds  25930  plyco0  25942  plypf1  25962  coeeulem  25974  coeidlem  25987  coeid3  25990  coemullem  26000  coemulhi  26004  coemulc  26005  dgradd2  26019  vieta1lem2  26061  dvtaylp  26119  musum  26932  perfectlem2  26970  dchrelbas3  26978  dchrmullid  26992  dchreq  26998  dchrsum  27009  gausslemma2dlem4  27109  dchrisum0re  27253  coltr  28166  lmieu  28303  elspansn5  31095  atomli  31903  pthisspthorcycl  34418  onsucconni  35626  poimirlem8  36800  poimirlem9  36801  poimirlem18  36810  poimirlem21  36813  poimirlem22  36814  poimirlem26  36818  lshpcmp  38162  lsator0sp  38175  atnle  38491  atlatmstc  38493  osumcllem8N  39138  osumcllem11N  39141  pexmidlem5N  39149  pexmidlem8N  39152  dochsat0  40632  dochexmidlem5  40639  dochexmidlem8  40642  fsuppind  41465  congabseq  42016  dflim5  42382  mnringmulrcld  43290  perfectALTVlem2  46689