In my experiences with Boolean algebra in dealing with logic gates for chip designs, there are a couple theorems which are slightly less natural, but get frequently used. Using * for our logical "and", in combination with + for our logical "or":

Covering Theorem
X * (X + Y) = X

Combining Theorem
(X + Y) * (X + Y') = X

Consensus Theorems
1. (X + Y) * (X' + Z) * (Y + Z) = (X + Y) * (X' + Z)
2. X * Y + X' * Z + Y * Z = X * Y + X' * Z

As previously mentioned, these theorems are slightly less intuitive in nature, but are quite useful.