MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  necon1bd Structured version   Visualization version   GIF version

Theorem necon1bd 2841
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
StepHypRef Expression
1 df-ne 2824 . . 3 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 necon1bd.1 . . 3 (𝜑 → (𝐴𝐵𝜓))
31, 2syl5bir 233 . 2 (𝜑 → (¬ 𝐴 = 𝐵𝜓))
43con1d 139 1 (𝜑 → (¬ 𝜓𝐴 = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1523  wne 2823
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 197  df-ne 2824
This theorem is referenced by:  necon4ad  2842  fvclss  6540  suppssr  7371  eceqoveq  7895  fofinf1o  8282  cantnfp1lem3  8615  cantnfp1  8616  mul0or  10705  inelr  11048  rimul  11049  rlimuni  14325  pc2dvds  15630  divsfval  16254  pleval2i  17011  lssvs0or  19158  lspsnat  19193  lmmo  21232  filssufilg  21762  hausflimi  21831  fclscf  21876  xrsmopn  22662  rectbntr0  22682  bcth3  23174  limcco  23702  ig1pdvds  23981  plyco0  23993  plypf1  24013  coeeulem  24025  coeidlem  24038  coeid3  24041  coemullem  24051  coemulhi  24055  coemulc  24056  dgradd2  24069  vieta1lem2  24111  dvtaylp  24169  musum  24962  perfectlem2  25000  dchrelbas3  25008  dchrmulid2  25022  dchreq  25028  dchrsum  25039  gausslemma2dlem4  25139  dchrisum0re  25247  coltr  25587  lmieu  25721  elspansn5  28561  atomli  29369  onsucconni  32561  poimirlem8  33547  poimirlem9  33548  poimirlem18  33557  poimirlem21  33560  poimirlem22  33561  poimirlem26  33565  lshpcmp  34593  lsator0sp  34606  atnle  34922  atlatmstc  34924  osumcllem8N  35567  osumcllem11N  35570  pexmidlem5N  35578  pexmidlem8N  35581  dochsat0  37063  dochexmidlem5  37070  dochexmidlem8  37073  congabseq  37858  perfectALTVlem2  41956
  Copyright terms: Public domain W3C validator