Theorem consensus

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 \( \psi \wedge \chi \) 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.)

Conclusion
\( \vdash \varphi \wedge \psi \vee \neg \varphi \wedge \chi \vee \psi \wedge \chi \leftrightarrow \varphi \wedge \psi \vee \neg \varphi \wedge \chi \)
Proof
l0
id
orc
l2
adantrr _
\( \vdash \varphi \wedge (\psi \wedge \chi) \rightarrow \varphi \wedge \psi \vee \neg \varphi \wedge \chi \)
olc
adantrl _
\( \vdash \neg \varphi \wedge (\psi \wedge \chi) \rightarrow \varphi \wedge \psi \vee \neg \varphi \wedge \chi \)
pm2.61ian l2 _
l6
jaoi l0 _
orc
impbii l6 _