Theorem consensus

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. (Contributed by NM, 16-May-2003) (Proof shortened by Andrew Salmon, 13-May-2011) (Proof shortened by Wolf Lammen, 20-Jan-2013)

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

Proof

Step	Hyp	Ref	Expression
1		id	|- ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) -> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
2		orc	|- ( ( ph /\ ps ) -> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
3	2	adantrr	|- ( ( ph /\ ( ps /\ ch ) ) -> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
4		olc	|- ( ( -. ph /\ ch ) -> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
5	4	adantrl	|- ( ( -. ph /\ ( ps /\ ch ) ) -> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
6	3 5	pm2.61ian	|- ( ( ps /\ ch ) -> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
7	1 6	jaoi	|- ( ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) \/ ( ps /\ ch ) ) -> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )
8		orc	|- ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) -> ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) \/ ( ps /\ ch ) ) )
9	7 8	impbii	|- ( ( ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) \/ ( ps /\ ch ) ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ ch ) ) )