Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > consensus  Unicode version 
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 lefthand side is redundant. (Contributed by NM, 16May2003.) (Proof shortened by Andrew Salmon, 13May2011.) (Proof shortened by Wolf Lammen, 20Jan2013.) 
Ref  Expression 

consensus 
Step  Hyp  Ref  Expression 

1  id 21  . . 3  
2  orc 376  . . . . 5  
3  2  adantrr 700  . . . 4 
4  olc 375  . . . . 5  
5  4  adantrl 699  . . . 4 
6  3, 5  pm2.61ian 768  . . 3 
7  1, 6  jaoi 370  . 2 
8  orc 376  . 2  
9  7, 8  impbii 182  1 
Colors of variables: wff set class 
Syntax hints: wn 5 wb 178 wo 359 wa 360 
This theorem was proved from axioms: ax1 7 ax2 8 ax3 9 axmp 10 
This theorem depends on definitions: dfbi 179 dfor 361 dfan 362 
Copyright terms: Public domain  W3C validator 