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

Theorem necon1bi 2686
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 2650 . . 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 1370  =/=wne 2648
This theorem is referenced by:  necon4ai  2691  fvbr0  5834  peano5  6632  1stnpr  6714  2ndnpr  6715  1st2val  6735  2nd2val  6736  eceqoveq  7339  mapprc  7352  ixp0  7430  setind  8091  hashfun  12357  hashf1lem2  12367  iswrdi  12397  dvdsrval  16913  thlle  18315  konigsberg  24077  hatomistici  26235  setindtr  29833  fourierdlem72  30708  afvpcfv0  30929
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