Is there a general result that theorems about finite structures proved in ZFC can be proved in ZF? 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.
 A: As long as your varieties have reasonable definitions, the axiom of choice will be eliminable from proofs like these.  The point is that any finite semigroup has an isomorphic copy whose underlying set consists of natural numbers, and that copy will be in Gödel's constructible universe $L$, where the axiom of choice holds.  So if there were a semigroup in $W$ that isn't in $V$, then the same would be true in $L$.
Now about that proviso "reasonable definitions": You can sneak a lot of set theory into the definition of a variety.  Consider the variety that consists of all groups if the continuum hypothesis holds and consists of all commutative semigroups if the continuum hypothesis fails.  With such "cheating" you can surely arrange for $W$ to be included in $V$ iff the axiom of choice holds.  My argument in the preceding paragraph tacitly assumed that the definitions of the varieties were absolute, in the sense that the constructible universe $L$ and the whole universe agree as to whether any particular finite semigroup is in the variety.  By working harder, one can get by with weaker absoluteness requirements, but one can't get rid of them completely.
A: There is a standard method to handle this kind of situation which uses the absoluteness of certain statements over models of set theory.
The basic idea is this. If you're investigating the properties of a certain "well-behaved" set $A$, then instead of working in the full set-theoretic universe $V$, you can work in the smallest universe $L[A]$ that contains $A$ and all the ordinal numbers. By classical results of Gödel and others, this smaller universe $L[A]$ satisfies some very strong forms of choice and many other nice properties. You can then freely use these facts to show that "$A$ has property $X$" holds in $L[A]$. As is this doesn't really mean much, but if "property $X$" is upward absolute, then you can conclude that "$A$ has property $X$" holds in the full set-theoretic universe $V$.
There are several tricks to analyze when a property is absolute or not. Many of them are syntactic in nature, for example Shoenfield's absoluteness theorem states that $\Sigma^1_3$ properties are always upward absolute. Assuming the existence of some large cardinals, a whole lot of statements can be shown to be absolute.
For the situation you describe, I believe everything is absolute for even simpler reasons. The constructible universe $L$ already contains isomorphic copies of all finite objects in the real universe $V$. Since the definition of a variety is finitary, varieties of finite semigroups are essentially the same in $L$ as they are in $V$. Therefore, inclusions of varieties of finite semigroups are absolute between $L$ and $V$. So you can freely use the axiom of choice in $L$ and the conclusions drawn automatically transfer from $L$ to $V$.
