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

Theorem necon2bi 2694
Description: Contrapositive inference for inequality. (Contributed by NM, 1-Apr-2007.)
Hypothesis
Ref Expression
necon2bi.1
Assertion
Ref Expression
necon2bi

Proof of Theorem necon2bi
StepHypRef Expression
1 necon2bi.1 . . 3
21neneqd 2659 . 2
32con2i 120 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  =wceq 1395  =/=wne 2652
This theorem is referenced by:  necon4iOLD  2702  minel  3882  rzal  3931  difsnb  4172  reusv7OLD  4664  dtrucor2  4686  kmlem6  8556  winainflem  9092  0npi  9281  0npr  9391  0nsr  9477  1div0  10233  rexmul  11492  rennim  13072  mrissmrcd  15037  prmirred  18525  prmirredOLD  18528  pthaus  20139  rplogsumlem2  23670  pntrlog2bndlem4  23765  pntrlog2bndlem5  23766  1div0apr  25176  subfacp1lem6  28629  itg2addnclem3  30068  sdrgacs  31150  rzalf  31392  jumpncnp  31701  fourierswlem  32013  bnj1311  34080  bj-dtrucor2v  34387  cdleme31id  36120
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