The title question is too vague so let me be specific.
Much of modern finite semigroup theory uses profinite semigroups and properties of profinite semigroups that depend on the existence of prime ideals in Boolean algebras, which is a choice principle weaker than AC. Often results are proved first via profinite methods and then explicit proofs using finite means are found later.
To narrow my question down, let me consider the following situation. Let V be what is sometimes called a variety of finite semigroups, that is, a class of finite semigroups closed under finite products, subsemigroups and homomorphic images. A pro-V semigroup is an inverse limit of semigroups in V. It is known, using Tychnoff's theorem for products of finite spaces, that every continuous finite quotient of a pro-V semigroup belongs to V. So if you want to show a variety W of finite semigroups is contained in a variety V it suffices to show each element of W is a continuous quotient of a free pro-V semigroup. Sometimes one has good information on the structure of free pro-V semigroups and can exploit this.
For example, Almeida proved that the smallest variety of finite semigroups containing all finite commutative semigroups and all finite groups is the variety of finite semigroups with central idempotents using the approach sketched above. Later Auinger gave a proof using only finite semigroups.
Question. Is there some general result in logic or set theory that would imply that the existence of a proof in ZF+Boolean prime ideal theoerem that a variety W of finite semigroups is contained in a variety V of finite semigroups implies the existence of a proof in ZF that W is contained in V?
Many results of this sort in finite semigroup theory were motivated by questions in automata theory and in principle one would like to avoid choice in this context.
Caveat: I know very little set theory or model theory so please take that into account in answer.