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

Theorem consensus 989
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 398 . . . . 5 ((𝜑𝜓) → ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
32adantrr 748 . . . 4 ((𝜑 ∧ (𝜓𝜒)) → ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
4 olc 397 . . . . 5 ((¬ 𝜑𝜒) → ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
54adantrl 747 . . . 4 ((¬ 𝜑 ∧ (𝜓𝜒)) → ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
63, 5pm2.61ian 826 . . 3 ((𝜓𝜒) → ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
71, 6jaoi 392 . 2 ((((𝜑𝜓) ∨ (¬ 𝜑𝜒)) ∨ (𝜓𝜒)) → ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
8 orc 398 . 2 (((𝜑𝜓) ∨ (¬ 𝜑𝜒)) → (((𝜑𝜓) ∨ (¬ 𝜑𝜒)) ∨ (𝜓𝜒)))
97, 8impbii 197 1 ((((𝜑𝜓) ∨ (¬ 𝜑𝜒)) ∨ (𝜓𝜒)) ↔ ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 194  wo 381  wa 382
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 195  df-or 383  df-an 384
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator