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

Theorem necon1bd 2671
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 2650 . . 3
2 necon1bd.1 . . 3
31, 2syl5bir 218 . 2
43con1d 124 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  =wceq 1370  =/=wne 2648
This theorem is referenced by:  necon4ad  2673  suppssrOLD  5960  fvclss  6084  suppssr  6854  eceqoveq  7339  fofinf1o  7727  cantnfp1lem3  8025  cantnfp1  8026  cantnfp1lem3OLD  8051  cantnfp1OLD  8052  mul0or  10113  inelr  10450  rimul  10451  rlimuni  13186  pc2dvds  14103  divsfval  14644  pleval2i  15293  lssvs0or  17367  lspsnat  17402  lmmo  19383  filssufilg  19883  hausflimi  19952  fclscf  19997  xrsmopn  20788  rectbntr0  20808  bcth3  21241  limcco  21768  ig1pdvds  22048  plyco0  22060  plypf1  22080  coeeulem  22092  coeidlem  22105  coeid3  22108  coemullem  22117  coemulhi  22121  coemulc  22122  dgradd2  22135  vieta1lem2  22177  dvtaylp  22235  musum  22931  perfectlem2  22969  dchrelbas3  22977  dchrmulid2  22991  dchreq  22997  dchrsum  23008  dchrisum0re  23162  coltr  23476  lmieu  23563  elspansn5  25446  atomli  26255  onsucconi  28739  congabseq  29777  lshpcmp  33484  lsator0sp  33497  atnle  33813  atlatmstc  33815  osumcllem8N  34458  osumcllem11N  34461  pexmidlem5N  34469  pexmidlem8N  34472  dochsat0  35953  dochexmidlem5  35960  dochexmidlem8  35963
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 185  df-ne 2650
  Copyright terms: Public domain W3C validator