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

Theorem consensus 926
 Description: The consensus theorem. This theorem and its dual (with and interchanged) are commonly used in computer logic design to eliminate redundant terms from Boolean expressions. Specifically, we prove that the term on the left-hand side is redundant. (Contributed by NM, 16-May-2003.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 20-Jan-2013.)
Assertion
Ref Expression
consensus

Proof of Theorem consensus
StepHypRef Expression
1 id 20 . . 3
2 orc 375 . . . . 5
32adantrr 698 . . . 4
4 olc 374 . . . . 5
54adantrl 697 . . . 4
63, 5pm2.61ian 766 . . 3
71, 6jaoi 369 . 2
8 orc 375 . 2
97, 8impbii 181 1
 Colors of variables: wff set class Syntax hints:   wn 3   wb 177   wo 358   wa 359 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361
 Copyright terms: Public domain W3C validator