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

Theorem necon1bd 2675
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 2654 . . 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 1395  =/=wne 2652
This theorem is referenced by:  necon4ad  2677  suppssrOLD  6021  fvclss  6154  suppssr  6950  eceqoveq  7435  fofinf1o  7821  cantnfp1lem3  8120  cantnfp1  8121  cantnfp1lem3OLD  8146  cantnfp1OLD  8147  mul0or  10214  inelr  10551  rimul  10552  rlimuni  13373  pc2dvds  14402  divsfval  14944  pleval2i  15594  lssvs0or  17756  lspsnat  17791  lmmo  19881  filssufilg  20412  hausflimi  20481  fclscf  20526  xrsmopn  21317  rectbntr0  21337  bcth3  21770  limcco  22297  ig1pdvds  22577  plyco0  22589  plypf1  22609  coeeulem  22621  coeidlem  22634  coeid3  22637  coemullem  22647  coemulhi  22651  coemulc  22652  dgradd2  22665  vieta1lem2  22707  dvtaylp  22765  musum  23467  perfectlem2  23505  dchrelbas3  23513  dchrmulid2  23527  dchreq  23533  dchrsum  23544  dchrisum0re  23698  coltr  24027  lmieu  24150  elspansn5  26492  atomli  27301  onsucconi  29902  congabseq  30912  lshpcmp  34713  lsator0sp  34726  atnle  35042  atlatmstc  35044  osumcllem8N  35687  osumcllem11N  35690  pexmidlem5N  35698  pexmidlem8N  35701  dochsat0  37184  dochexmidlem5  37191  dochexmidlem8  37194
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 2654
  Copyright terms: Public domain W3C validator