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

Theorem consensus 998
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 400 . . . . 5 ((𝜑𝜓) → ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
32adantrr 752 . . . 4 ((𝜑 ∧ (𝜓𝜒)) → ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
4 olc 399 . . . . 5 ((¬ 𝜑𝜒) → ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
54adantrl 751 . . . 4 ((¬ 𝜑 ∧ (𝜓𝜒)) → ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
63, 5pm2.61ian 830 . . 3 ((𝜓𝜒) → ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
71, 6jaoi 394 . 2 ((((𝜑𝜓) ∨ (¬ 𝜑𝜒)) ∨ (𝜓𝜒)) → ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
8 orc 400 . 2 (((𝜑𝜓) ∨ (¬ 𝜑𝜒)) → (((𝜑𝜓) ∨ (¬ 𝜑𝜒)) ∨ (𝜓𝜒)))
97, 8impbii 199 1 ((((𝜑𝜓) ∨ (¬ 𝜑𝜒)) ∨ (𝜓𝜒)) ↔ ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wo 383  wa 384
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 197  df-or 385  df-an 386
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator