According to Wikipedia,
A powerful and nontrivial metatheorem states that any theorem of 𝟐 holds for all Boolean algebras. Conversely, an identity that holds for an arbitrary nontrivial Boolean algebra also holds in 𝟐. Hence all the mathematical content of Boolean algebra is captured by 𝟐.
What this means is that if $\phi = \psi$ is an equation in Boolean algebra, involving any number of variables, then $\phi = \psi$ holds in all Boolean algebras iff it holds in the two-element Boolean algebra 𝟐, i.e., when the variables are only allowed to have the values $0,1$. This means that $\phi = \psi$ can be proved using any complete axiomatization of Boolean algebras, for example Huntington's.
Let's sketch how to prove this theorem. In order to reduce confusion, let us write $\phi \stackrel{0,1}= \psi$ if $\phi(\alpha) = \psi(\alpha)$ for any $0,1$-evaluation of the variables in $\phi,\psi$, and let us write $\phi \approx \psi$ if the axioms of Boolean algebra imply that $\phi = \psi$. We would like to show that $\phi \stackrel{0,1}= \psi$ iff $\phi \approx \psi$. The proof is by induction on the number of variables.
If $\phi,\psi$ involve no variables then $\phi \stackrel{0,1}= b \stackrel{0,1}= \psi$ for some $b \in \{0,1\}$. Simple structural induction shows that if $\phi \stackrel{0,1}= b$ then $\phi \approx b$, completing the proof in this case.
For the inductive case, let $x$ be an arbitrary variable appearing in $\phi$ and $\psi$. Define $N[\phi] = (x \land \phi|_{x=1}) \lor (\lnot x \land \phi|_{x=0})$. If we $\phi \stackrel{0,1}= \psi$ then $\phi|_{x=b} \stackrel{0,1}= \psi|_{x=b}$ for $b \in \{0,1\}$. The inductive hypothesis shows that $\phi_{x=b} \approx \psi_{x=b}$ for $b \in \{0,1\}$, and it easily follows that $N[\phi] \approx N[\psi]$. Hence to complete the proof, all we need to do is show that $\phi \approx N[\phi]$.
We show that $\phi \approx N[\phi]$ by structural induction. This amounts to proving finitely many identities involving finitely many variables. The base cases $\phi=0,1,x,y$ (where $y \neq x$ is a variable) are easy. There are three inductive cases for the three connectives $\lnot,\lor,\land$. As an example, consider $\phi = \lnot \chi$. We know that $\chi \approx N[\chi]$, and would like to derive $\lnot \chi \approx N[\lnot \chi]$. This amounts to proving
$$
\lnot [(x \land \chi|_{x=1}) \lor (\lnot x \land \chi_{x=0})] \approx
(x \land \lnot \chi|_{x=1}) \lor (\lnot x \land \lnot \chi_{x=0}),
$$
an equation in three variables.
Finding the minimal expression equivalent to a given one is hard. Indeed, given a DNF, determining whether the minimal equivalent expression has size 1 is NP-complete (since it is easy to check whether a given DNF is a tautology).
The Formula-MCSP problem is, given a truth table of a function and a parameter $s$, to determine whether the function can be represented by a formula of size at most $s$. It is conjectured that Formula-MCSP is NP-complete. Your problem is likely harder: variants are known to be $\Pi_2^p$-complete.
In some cases, we can provably show that some equations are hard to prove. For example, suppose that we want to prove that a CNF is unsatisfiable (equals 0), and that we are only allowed to use rearrangement laws (commutativity and associativity of $\lor$ and $\land$), absorption laws ($a \land a = a$ and $a \lor a = a$), constant absorption laws, and the Resolution rule $(a \lor b) \land (\lnot a \lor c) \approx b \lor c$. This axiomatization is complete — if the CNF is unsatisfiable then it can prove that it equals 0 — but explicit examples are known in which every proof has size which is exponential in the number of variables.
