It is a classical result, due to Birkhoff, that equational logic is complete; that is, if $\Sigma$ is a classical (finitary) signature in the sense of universal algebra and $s, t$ are terms constructed from variables and the operation symbols of $\Sigma$, then the equation $s = t$ is deducible from a set of equations $E$ (using the standard rules of equational reasoning) if and only if the equation $s = t$ is entailed by $E$, i.e. is satisfied by every $\Sigma$-algebra that satisfies all equations of $E$.
My question is: what are the useful consequences of the completeness of equational logic? I suppose that one useful consequence would be its compactness, i.e. that if $s = t$ is entailed by a set of equations $E$, then it is entailed by a finite subset of $E$. What are some other (significant) useful consequences of knowing that equational logic is complete?