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 1542   ≠ 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  7196  suppssr  8145  suppssrg  8146  suppofssd  8153  eceqoveq  8769  fofinf1o  9242  cantnfp1lem3  9601  cantnfp1  9602  mul0or  11790  rimul  12150  rlimuni  15512  pc2dvds  16850  divsfval  17511  pleval2i  18300  lssvs0or  21108  lspsnat  21143  psdmul  22132  lmmo  23345  filssufilg  23876  hausflimi  23945  fclscf  23990  xrsmopn  24778  rectbntr0  24798  bcth3  25298  limcco  25860  ig1pdvds  26145  plyco0  26157  plypf1  26177  coeeulem  26189  coeidlem  26202  coeid3  26205  coemullem  26215  coemulhi  26219  coemulc  26220  dgradd2  26233  vieta1lem2  26277  dvtaylp  26335  musum  27154  perfectlem2  27193  dchrelbas3  27201  dchrmullid  27215  dchreq  27221  dchrsum  27232  gausslemma2dlem4  27332  dchrisum0re  27476  muls0ord  28177  coltr  28715  lmieu  28852  pthisspthorcycl  29870  elspansn5  31645  atomli  32453  onsucconni  36619  poimirlem8  37949  poimirlem9  37950  poimirlem18  37959  poimirlem21  37962  poimirlem22  37963  poimirlem26  37967  lshpcmp  39434  lsator0sp  39447  atnle  39763  atlatmstc  39765  osumcllem8N  40409  osumcllem11N  40412  pexmidlem5N  40420  pexmidlem8N  40423  dochsat0  41903  dochexmidlem5  41910  dochexmidlem8  41913  aks6d1c4  42563  sn-remul0ord  42840  fsuppind  43023  congabseq  43402  dflim5  43757  mnringmulrcld  44655  perfectALTVlem2  48198