Theorem necon2bi 2690

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 2655	. 2
3	2	con2i 120	1

Syntax hints:  -.wn 3  ->wi 4  =wceq 1370  =/=wne 2648

This theorem is referenced by:  necon4iOLD  2698  minel  3848  rzal  3895  difsnb  4132  reusv7OLD  4621  dtrucor2  4643  kmlem6  8461  winainflem  8997  0npi  9188  0npr  9298  0nsr  9383  renfdisj  9574  1div0  10132  rexmul  11373  rennim  12886  mrissmrcd  14737  prmirred  18112  prmirredOLD  18115  pthaus  19610  rplogsumlem2  23134  pntrlog2bndlem4  23229  pntrlog2bndlem5  23230  1div0apr  24130  subfacp1lem6  27529  itg2addnclem3  28905  sdrgacs  30018  rzalf  30199  jumpncnp  30466  fourierswlem  30760  bnj1311  32858  bj-dtrucor2v  33167  cdleme31id  34889

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 2650