Consensus theorem

Boolean algebra: XY + X'Z + YZ = XY + X'Z where YZ, the algebraically redundant term, is called the "consensus term", or its dual form (X + Y)(X' + Z)(Y + Z) = (X + Y)(X' + Z), in which case Y + Z is the consensus term. (Note: X+Y, X'+Z \vdash Y+Z is an example of the resolution inference rule (replacing the + with \vee and the prime with prefix \neg might make this more evident).)