consensus - Metamath Proof Explorer

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

Theorem consensus 999

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**
Step	Hyp	Ref	Expression
1		id 22	. . 3 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
2		orc 400	. . . . 5 $/\$ $/\$ $\/$ $/\$
3	2	adantrr 753	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$
4		olc 399	. . . . 5 $/\$ $/\$ $\/$ $/\$
5	4	adantrl 752	. . . 4 $/\$ $/\$ $/\$ $\/$ $/\$
6	3, 5	pm2.61ian 831	. . 3 $/\$ $/\$ $\/$ $/\$
7	1, 6	jaoi 394	. 2 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
8		orc 400	. 2 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$
9	7, 8	impbii 199	1 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wb 196 $\/$ wo 383 $/\$ wa 384

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 197 df-or 385 df-an 386

This theorem is referenced by: (None)

W3C validator