Theorem consensus 574

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 show the term (ψ ∧ χ) on the left-hand side is redundant.

Assertion

Ref	Expression
consensus	⊢ ((((φ ∧ ψ) ∨ (¬ φ ∧ χ)) ∨ (ψ ∧ χ)) ↔ ((φ ∧ ψ) ∨ (¬ φ ∧ χ)))

Proof of Theorem consensus

Step	Hyp	Ref	Expression
1		id 9	. . 3™/SPAN> ⊢ (((φ ∧ ψ) ∨ (¬ φ ∧ χ)) → ((φ ∧ ψ) ∨ (¬ φ ∧ χ)))
2		dedlema 569	. . . . . . 7 ⊢ (φ → (ψ ↔ ((ψ ∧ φ) ∨ (χ ∧ ¬ φ))))
3	2	biimpd 135	. . . . . 6 ⊢ (φ → (ψ → ((ψ ∧ φ) ∨ (χ ∧ ¬ φ))))
4	3	adantrd 308	. . . . 5 ⊢ (φ → ((ψ ∧ χ) → ((ψ ∧ φ) ∨ (χ ∧ ¬ φ))))
5		dedlemb 570	. . . . . . 7 ⊢ (¬ φ → (χ ↔ ((ψ ∧ φ) ∨ (χ ∧ ¬ φ))))
6	5	biimpd 135	. . . . . 6 ⊢ (¬ φ → (χ → ((ψ ∧ φ) ∨ (χ ∧ ¬ φ))))
7	6	adantld 307	. . . . 5 ⊢ (¬ φ → ((ψ ∧ χ) → ((ψ ∧ φ) ∨ (χ ∧ ¬ φ))))
8	4, 7	pm2.61i 110	. . . 4 ⊢ ((ψ ∧ χ) → ((ψ ∧ φ) ∨ (&cöi; ∧ ¬ φ)))
9		ancom 333	. . . . 5 ⊢ ((ψ ∧ φ) ↔ (φ ∧ ψ))
10		ancom 333	. . . . 5 ⊢ ((χ ∧ ¬ φ) ↔ (¬ φ ∧ χ))
11	9, 10	orbi12i 216	. . . 4 ⊢ (((ψ ∧ φ) ∨ (χ ∧ ¬ φ)) ↔ ((φ ∧ ψ) ∨ (¬ φ ∧ χ)))
12	8, 11	sylib 173	. . 3 ⊢ ((ψ ∧ χ) → ((φ ∧ ψ) ∨ (¬ φ ∧ χ)))
13	1, 12	jaoi 275	. 2 ⊢ ((((φ ∧ ψ) ∨ (¬ φ ∧ χ)) ∨ (ψ ∧ χ)) → ((φ ∧ ψ) ∨ (¬ φ ∧ χ)))
14		orc 225	. 2 ⊢ (((φ ∧ ψ) ∨ (¬ φ ∧ χ)) → (((φ ∧ ψ) ∨ (¬ φ ∧ χ)) ∨ (ψ ∧ χ)))
15	13, 14	impbi 139	1 ⊢ ((((φ ∧ ψ) ∨ (¬ φ ∧ χ)) ∨ (ψ ∧ χ)) ↔ ((φ ∧ ψ) ∨ (¬ φ ∧ χ)))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∨ wo 195   ∧ wa 196

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198

metamath.org