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

Theorem necon1bi 2690
Description: Contrapositive inference for inequality. (Contributed by NM, 18-Mar-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 22-Nov-2019.)
Hypothesis
Ref Expression
necon1bi.1
Assertion
Ref Expression
necon1bi

Proof of Theorem necon1bi
StepHypRef Expression
1 df-ne 2654 . . 3
2 necon1bi.1 . . 3
31, 2sylbir 213 . 2
43con1i 129 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  =wceq 1395  =/=wne 2652
This theorem is referenced by:  necon4ai  2695  fvbr0  5892  peano5  6723  1stnpr  6804  2ndnpr  6805  1st2val  6826  2nd2val  6827  eceqoveq  7435  mapprc  7443  ixp0  7522  setind  8186  hashfun  12495  hashf1lem2  12505  iswrdi  12552  dvdsrval  17294  thlle  18728  konigsberg  24987  hatomistici  27281  mppsval  28932  setindtr  30966  fourierdlem72  31961  afvpcfv0  32231
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