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

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
StepHypRef Expression
1 necon2bi.1 . . 3
21neneqd 2655 . 2
32con2i 120 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator