This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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