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	$⊢ (((φ \land ψ) \lor (\neg φ \land χ)) \lor (ψ \land χ)) \leftrightarrow ((φ \land ψ) \lor (\neg φ \land χ))$

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ ((φ \land ψ) \lor (\neg φ \land χ)) \to ((φ \land ψ) \lor (\neg φ \land χ))$
2		orc	$⊢ (φ \land ψ) \to ((φ \land ψ) \lor (\neg φ \land χ))$
3	2	adantrr	$⊢ (φ \land (ψ \land χ)) \to ((φ \land ψ) \lor (\neg φ \land χ))$
4		olc	$⊢ (\neg φ \land χ) \to ((φ \land ψ) \lor (\neg φ \land χ))$
5	4	adantrl	$⊢ (\neg φ \land (ψ \land χ)) \to ((φ \land ψ) \lor (\neg φ \land χ))$
6	3 5	pm2.61ian	$⊢ (ψ \land χ) \to ((φ \land ψ) \lor (\neg φ \land χ))$
7	1 6	jaoi	$⊢ (((φ \land ψ) \lor (\neg φ \land χ)) \lor (ψ \land χ)) \to ((φ \land ψ) \lor (\neg φ \land χ))$
8		orc	$⊢ ((φ \land ψ) \lor (\neg φ \land χ)) \to (((φ \land ψ) \lor (\neg φ \land χ)) \lor (ψ \land χ))$
9	7 8	impbii	$⊢ (((φ \land ψ) \lor (\neg φ \land χ)) \lor (ψ \land χ)) \leftrightarrow ((φ \land ψ) \lor (\neg φ \land χ))$

Metamath Proof Explorer

Theorem consensus

Proof