MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  consensus Structured version   Visualization version   GIF version

Theorem consensus 1052
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 (𝜓𝜒) 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.)
Assertion
Ref Expression
consensus ((((𝜑𝜓) ∨ (¬ 𝜑𝜒)) ∨ (𝜓𝜒)) ↔ ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))

Proof of Theorem consensus
StepHypRef Expression
1 id 22 . . 3 (((𝜑𝜓) ∨ (¬ 𝜑𝜒)) → ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
2 orc 866 . . . . 5 ((𝜑𝜓) → ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
32adantrr 716 . . . 4 ((𝜑 ∧ (𝜓𝜒)) → ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
4 olc 867 . . . . 5 ((¬ 𝜑𝜒) → ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
54adantrl 715 . . . 4 ((¬ 𝜑 ∧ (𝜓𝜒)) → ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
63, 5pm2.61ian 811 . . 3 ((𝜓𝜒) → ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
71, 6jaoi 856 . 2 ((((𝜑𝜓) ∨ (¬ 𝜑𝜒)) ∨ (𝜓𝜒)) → ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
8 orc 866 . 2 (((𝜑𝜓) ∨ (¬ 𝜑𝜒)) → (((𝜑𝜓) ∨ (¬ 𝜑𝜒)) ∨ (𝜓𝜒)))
97, 8impbii 208 1 ((((𝜑𝜓) ∨ (¬ 𝜑𝜒)) ∨ (𝜓𝜒)) ↔ ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 397  wo 846
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator