"Let $T'$ be obtained from $T$ by adding new constants $e_1,e_2,...,e_n$ (but no new nonlogical axioms). For every formula $A$ of $T$, and every sequence of constants $e_1,e_2,...,e_n$, $\vdash _TA$ iff $\vdash_{T'}A[e_1,e_2,...,e_n]$."
It sounds like the theorem asserts that if an instance of a formula $A$ is provable for certain constants, then it must be provable for in general form, when those constants are replaced by free variables. This doesn't make much intuitive sense to me, and I'm not entirely sure I see how it follows from the substitution theorem, so for clarity's sake, I'd appreciate it if someone could correct me.
Edit: so it is the only if side that confuses me
The Substitution Rule part: once you have the proof of $A[e_1, ..., e_n]$ in $T'$ you may be tempted to prove $A$ in $T$ by simply replacing $e_1, ..., e_n$ by the appropriate $x_1, ..., x_n$ throughout the first proof. However, some of these variables may have been used in that proof, so they may interfere with the ones you've just inserted and ruin everything. The solution is to replace $e_1, ..., e_n$ by some $y_1, ..., y_n$ that weren't used in the proof. Now you have $\vdash_TA[y_1, ..., y_n]$ and by the substitution rule $\vdash_TA[x_1, ..., x_n]$ which is the same as $\vdash_TA$.