Theorem consensus 844

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 (ps /\ ch) on the left-hand side is redundant. (The proof was shortened by Andrew Salmon, 13-May-2011.)

Assertion

Ref	Expression
consensus	|- ((((ph /\ ps) \/ (-. ph /\ ch)) \/ (ps /\ ch)) <-> ((ph /\ ps) \/ (-. ph /\ ch)))

Proof of Theorem consensus

Step	Hyp	Ref	Expression
1		id 73	. . 3 |- (((ph /\ ps) \/ (-. ph /\ ch)) -> ((ph /\ ps) \/ (-. ph /\ ch)))
2		pm3.21 306	. . . . . . . . . 10 |- (ps -> (ph -> (ph /\ ps)))
3	2	con3d 111	. . . . . . . . 9 |- (ps -> (-. (ph /\ ps) -> -. ph))
4	3	com12 14	. . . . . . . 8 |- (-. (ph /\ ps) -> (ps -> -. ph))
5	4	anim1d 619	. . . . . . 7 |- (-. (ph /\ ps) -> ((ps /\ ch) -> (-. ph /\ ch)))
6	5	con3d 111	. . . . . 6 |- (-. (ph /\ ps) -> (-. (-. ph /\ ch) -> -. (ps /\ ch)))
7	6	imp 377	. . . . 5 |- ((-. (ph /\ ps) /\ -. (-. ph /\ ch)) -> -. (ps /\ ch))
8	7	con2i 113	. . . 4 |- ((ps /\ ch) -> -. (-. (ph /\ ps) /\ -. (-. ph /\ ch)))
9		oran 338	. . . 4 |- (((ph /\ ps) \/ (-. ph /\ ch)) <-> -. (-. (ph /\ ps) /\ -. (-. ph /\ ch)))
10	8, 9	sylibr 217	. . 3 |- ((ps /\ ch) -> ((ph /\ ps) \/ (-. ph /\ ch)))
11	1, 10	jaoi 368	. 2 |- ((((ph /\ ps) \/ (-. ph /\ ch)) \/ (ps /\ ch)) -> ((ph /\ ps) \/ (-. ph /\ ch)))
12		orc 291	. 2 |- (((ph /\ ps) \/ (-. ph /\ ch)) -> (((ph /\ ps) \/ (-. ph /\ ch)) \/ (ps /\ ch)))
13	11, 12	impbii 174	1 |- ((((ph /\ ps) \/ (-. ph /\ ch)) \/ (ps /\ ch)) <-> ((ph /\ ps) \/ (-. ph /\ ch)))

Syntax hints:  -. wn 2   <-> wb 163   \/ wo 239   /\ wa 240

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242

Copyright terms: Public domain