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	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) ∨ ( 𝜓 ∧ 𝜒 ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) → ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) )
2		orc	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) )
3	2	adantrr	⊢ ( ( 𝜑 ∧ ( 𝜓 ∧ 𝜒 ) ) → ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) )
4		olc	⊢ ( ( ¬ 𝜑 ∧ 𝜒 ) → ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) )
5	4	adantrl	⊢ ( ( ¬ 𝜑 ∧ ( 𝜓 ∧ 𝜒 ) ) → ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) )
6	3 5	pm2.61ian	⊢ ( ( 𝜓 ∧ 𝜒 ) → ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) )
7	1 6	jaoi	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) ∨ ( 𝜓 ∧ 𝜒 ) ) → ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) )
8		orc	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) → ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) ∨ ( 𝜓 ∧ 𝜒 ) ) )
9	7 8	impbii	⊢ ( ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) ∨ ( 𝜓 ∧ 𝜒 ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) )