I have two simple questions.
A) Does Birkhoff's completeness theorem follow directly from Gödel's completeness theorem?
B) Is Birkhoff's completeness theorem constructive in the following sense: Given a semantic proof in universal algebra, can we explicitly construct a syntactic proof out of it?
A) A completeness theorem for a logic says that $T\models \phi$ if and only if $T\vdash \phi$, that is, every model of $T$ satifies $\phi$ if and only if there is a proof of $\phi$ from $T$. To make sense of this statement, we have to fix a proof system for our logic - completeness theorems are about logics together with notions of syntactic consequence.
Gödel's completeness theorem says that first-order logic with a standard proof system is complete, and Birkhoff's completeness theorem says equational logic with a standard proof system is complete. Now, equational logic sits naturally inside first-order logic, so Gödel's completeness theorem tells us that if there's an equation $\phi$ which is (semantically) implied by some equational axioms $T$, then there's a first-order proof of $\phi$ from $T$. For all we know, this first-order proof might meander far outside the bounds of equational logic.
Birkhoff's completeness theorem strengthens this by saying that a proof can be found in our equational proof system.
B) I don't know for sure, but I would be very surprised if the answer was yes.