In standard, first-order predicate logic suppose that with a set of assumptions $\Gamma$ I can deduce $$\Gamma\cup\{A(a),B(m),\forall x\forall y\exists z[A(x)\land B(y)\rightarrow C(x,y,z)]\}\vdash D(b)$$ for $A(x),\ B(y),\ C(x,y,z),\ \text{and}\ D(z)$ well-formed formulae free in the indicated variables. Knowing this, can I then deduce the following? $$ \Gamma\cup\{A(a),D(b),\forall x\forall z\exists y[A(x)\land D(z)\rightarrow C(x,y,z)]\}\vdash \exists yB(y) $$ where all wffs are the same as above (but note the change in which variable is existentially quantified in $C$).
I am not sure whether I can apply the deduction theorem here (because I think I would have to make use of Generalization over $D$). Furthermore, it's not clear to me that even if I could apply deduction theorem that it would get me very far. I suspect that this proof is a dead-end, but I'm having difficulty grasping precisely why.
So, can I apply deduction theorem to the first (even if I Generalize $D$)? And can I deduce the second from the first? Why, or why not? All advice on proof strategies welcome!
Your second formula does not follow from the first: consider the case where $\Gamma$ is empty, $A$ and $D$ are the 1-ary and $C$ the 3-ary "always true" predicates, and $B$ is the 1-ary "always false" predicate. Then the first entailment is satisfied and the second is not.
You can't use the deduction theorem, because B(m) is not among the assumptions of the second entailment. You can use metatheoretic reasoning to eliminate assumptions from entailments: if $\Gamma \vdash A$ and $\Gamma, A \vdash B$, then $\Gamma \vdash B$, but you need more than just the deduction theorem to prove this, and you won't be able to eliminate $B(m)$ from your assumptions without being given more.