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

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

Proof of Theorem necon4bd
StepHypRef Expression
1 necon4bd.1 . . 3
21necon2bd 2672 . 2
3 notnot2 112 . 2
42, 3syl6 33 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  =wceq 1395  =/=wne 2652
This theorem is referenced by:  om00  7243  pw2f1olem  7641  xlt2add  11481  hashfun  12495  hashtpg  12523  fsumcl2lem  13553  fprodcl2lem  13757  gcdeq0  14159  phibndlem  14300  abvn0b  17951  cfinufil  20429  isxmet2d  20830  i1fres  22112  tdeglem4  22458  ply1domn  22524  pilem2  22847  isnsqf  23409  ppieq0  23450  chpeq0  23483  chteq0  23484  lcmeq0  31206  bcc0  31245  ltrnatlw  35908
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