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 1541   ≠ 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  7194  suppssr  8132  suppssrg  8133  suppofssd  8139  eceqoveq  8768  fofinf1o  9278  cantnfp1lem3  9625  cantnfp1  9626  mul0or  11804  inelr  12152  rimul  12153  rlimuni  15444  pc2dvds  16762  divsfval  17443  pleval2i  18239  lssvs0or  20630  lspsnat  20665  lmmo  22768  filssufilg  23299  hausflimi  23368  fclscf  23413  xrsmopn  24212  rectbntr0  24232  bcth3  24732  limcco  25294  ig1pdvds  25578  plyco0  25590  plypf1  25610  coeeulem  25622  coeidlem  25635  coeid3  25638  coemullem  25648  coemulhi  25652  coemulc  25653  dgradd2  25666  vieta1lem2  25708  dvtaylp  25766  musum  26577  perfectlem2  26615  dchrelbas3  26623  dchrmullid  26637  dchreq  26643  dchrsum  26654  gausslemma2dlem4  26754  dchrisum0re  26898  coltr  27652  lmieu  27789  elspansn5  30579  atomli  31387  pthisspthorcycl  33809  onsucconni  34985  poimirlem8  36159  poimirlem9  36160  poimirlem18  36169  poimirlem21  36172  poimirlem22  36173  poimirlem26  36177  lshpcmp  37523  lsator0sp  37536  atnle  37852  atlatmstc  37854  osumcllem8N  38499  osumcllem11N  38502  pexmidlem5N  38510  pexmidlem8N  38513  dochsat0  39993  dochexmidlem5  40000  dochexmidlem8  40003  fsuppind  40823  congabseq  41356  dflim5  41722  mnringmulrcld  42630  perfectALTVlem2  46034