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

Theorem necon2bbid 2713
Description: Contrapositive deduction for inequality. (Contributed by NM, 13-Apr-2007.) (Proof shortened by Wolf Lammen, 24-Nov-2019.)
Hypothesis
Ref Expression
necon2bbid.1
Assertion
Ref Expression
necon2bbid

Proof of Theorem necon2bbid
StepHypRef Expression
1 notnot 291 . . 3
2 necon2bbid.1 . . 3
31, 2syl5rbbr 260 . 2
43necon4abid 2708 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  =wceq 1395  =/=wne 2652
This theorem is referenced by:  necon4bid  2716  omwordi  7239  omass  7248  nnmwordi  7303  sdom1  7739  pceq0  14394  f1otrspeq  16472  pmtrfinv  16486  symggen  16495  psgnunilem1  16518  mdetralt  19110  mdetunilem7  19120  ftalem5  23350  fsumvma  23488  dchrelbas4  23518  fsumcvg4  27932  lkreqN  34895
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