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

Theorem consensus 1046
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 863 . . . . 5 ((𝜑𝜓) → ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
32adantrr 715 . . . 4 ((𝜑 ∧ (𝜓𝜒)) → ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
4 olc 864 . . . . 5 ((¬ 𝜑𝜒) → ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
54adantrl 714 . . . 4 ((¬ 𝜑 ∧ (𝜓𝜒)) → ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
63, 5pm2.61ian 810 . . 3 ((𝜓𝜒) → ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
71, 6jaoi 853 . 2 ((((𝜑𝜓) ∨ (¬ 𝜑𝜒)) ∨ (𝜓𝜒)) → ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
8 orc 863 . 2 (((𝜑𝜓) ∨ (¬ 𝜑𝜒)) → (((𝜑𝜓) ∨ (¬ 𝜑𝜒)) ∨ (𝜓𝜒)))
97, 8impbii 211 1 ((((𝜑𝜓) ∨ (¬ 𝜑𝜒)) ∨ (𝜓𝜒)) ↔ ((𝜑𝜓) ∨ (¬ 𝜑𝜒)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 208  wa 398  wo 843
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 209  df-an 399  df-or 844
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator