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

Theorem necon4ad 2677
Description: Contrapositive inference for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 23-Nov-2019.)
Hypothesis
Ref Expression
necon4ad.1
Assertion
Ref Expression
necon4ad

Proof of Theorem necon4ad
StepHypRef Expression
1 notnot1 122 . 2
2 necon4ad.1 . . 3
32necon1bd 2675 . 2
41, 3syl5 32 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  =wceq 1395  =/=wne 2652
This theorem is referenced by:  necon1d  2682  fisseneq  7751  f1finf1o  7766  dfac5  8530  isf32lem9  8762  fpwwe2  9042  qextlt  11431  qextle  11432  xsubge0  11482  hashf1  12506  climuni  13375  rpnnen2  13959  fzo0dvdseq  14039  4sqlem11  14473  haust1  19853  deg1lt0  22491  ply1divmo  22536  ig1peu  22572  dgrlt  22663  quotcan  22705  fta  23353  atcv0eq  27298  erdszelem9  28643  jm2.19  30935  jm2.26lem3  30943  dgraa0p  31098  lshpdisj  34712  lsatcv0eq  34772  exatleN  35128  atcvr0eq  35150  cdlemg31c  36425
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