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

Theorem necon1bi 2674
 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 2638 . . 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 1381   wne 2636 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 2638 This theorem is referenced by:  necon4ai  2679  fvbr0  5873  peano5  6704  1stnpr  6785  2ndnpr  6786  1st2val  6807  2nd2val  6808  eceqoveq  7414  mapprc  7422  ixp0  7500  setind  8163  hashfun  12469  hashf1lem2  12479  iswrdi  12526  dvdsrval  17162  thlle  18595  konigsberg  24852  hatomistici  27146  mppsval  28798  setindtr  30934  fourierdlem72  31846  afvpcfv0  32065
 Copyright terms: Public domain W3C validator