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

Theorem necon4d 2684
Description: Contrapositive inference for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypothesis
Ref Expression
necon4d.1
Assertion
Ref Expression
necon4d

Proof of Theorem necon4d
StepHypRef Expression
1 necon4d.1 . . 3
21necon2bd 2672 . 2
3 nne 2658 . 2
42, 3syl6ib 226 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  =wceq 1395  =/=wne 2652
This theorem is referenced by:  oa00  7227  map0g  7478  epfrs  8183  fin23lem24  8723  abs00  13122  oddvds  16571  isabvd  17469  01eq0ring  17920  uvcf1  18823  lindff1  18855  hausnei2  19854  dfcon2  19920  hausflimi  20481  hauspwpwf1  20488  cxpeq0  23059  his6  26016  nn0sqeq1  27562  rpnnen3  30974  lkreqN  34895  ltrnideq  35900  hdmapip0  37645
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