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

Step	Hyp	Ref	Expression
1		necon2bi.1	. . 3
2	1	neneqd 2659	. 2
3	2	con2i 120	1

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