Theorem necon1bd 2974

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1559   ≠ wne 2956

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 209  df-ne 2957

This theorem is referenced by:  necon4ad  2975  fvclss  7220  suppssr  8169  suppssrg  8170  suppofssd  8177  eceqoveq  8798  fofinf1o  9269  cantnfp1lem3  9629  cantnfp1  9630  mul0or  11821  rimul  12180  rlimuni  15568  pc2dvds  16906  divsfval  17568  pleval2i  18357  lssvs0or  21168  lspsnat  21203  psdmul  22219  lmmo  23428  filssufilg  23959  hausflimi  24028  fclscf  24073  xrsmopn  24861  rectbntr0  24881  bcth3  25381  limcco  25943  ig1pdvds  26228  plyco0  26240  plypf1  26260  coeeulem  26272  coeidlem  26285  coeid3  26288  coemullem  26298  coemulhi  26302  coemulc  26303  dgradd2  26316  vieta1lem2  26363  dvtaylp  26421  musum  27243  perfectlem2  27282  dchrelbas3  27290  dchrmullid  27304  dchreq  27310  dchrsum  27321  gausslemma2dlem4  27421  dchrisum0re  27565  muls0ord  28266  coltr  28804  lmieu  28941  pthisspthorcycl  29959  elspansn5  31734  atomli  32542  onsucconni  36758  poimirlem8  38088  poimirlem9  38089  poimirlem18  38098  poimirlem21  38101  poimirlem22  38102  poimirlem26  38106  lshpcmp  39573  lsator0sp  39586  atnle  39902  atlatmstc  39904  osumcllem8N  40548  osumcllem11N  40551  pexmidlem5N  40559  pexmidlem8N  40562  dochsat0  42042  dochexmidlem5  42049  dochexmidlem8  42052  aks6d1c4  42702  sn-remul0ord  42978  fsuppind  43133  congabseq  43512  dflim5  43867  mnringmulrcld  44765  perfectALTVlem2  48305