Very simple predicate logic deduction question I am very new to logic and currently taking a course about it but unfortunately it's a weekend now so I can't get the answers I need! 
Basically I am wondering a very basic thing. I want to prove something with natural deduction and let's say I have this premise:
Ok so let's start the question, here's an example but not a full example, just a short bit:
$$\forall x\forall y\big(A(x)\to B(y)\big)\qquad\text{(premise)}$$
So we got these two variables $x$ and $y$ and then just get rid of the quantifiers and replace the variables with two arbitrary constants just like the rule says: 
$$A(c)\to B(d)$$
Okay now for the question... Let's also say that I have another premise, or perhaps just an assumption even, that says: 
$$A(d)$$
Would it be usable with $A(c)$? Like, could I use the modus ponens rule like this:
$$A(d)\quad A(c) \to B(d)$$
The two constants $d$ and $c$ are different. I'mma guess the answer to this question is in fact "no" but it's something that keeps bothering me (because I always go like "Hmm but I can do this to appl--Oh... Guess not...)" and I just want to 100% make sure it's not possible since I am absolutely horrible at this subject! 
 A: In natural deduction, you may deduce $P(t)$ from $\forall x\: P(x)$ for arbitrary terms $t$.
Thus, in your case, you can deduce $A(d) \rightarrow B(d)$ from $\forall x\forall y\: (A(x)\rightarrow B(y))$, and then use the premise $A(d)$ to deduce $B(d)$.
You can generalize that by instead deducing $A(d) \rightarrow B(t)$ from $\forall x\forall y\: (A(x)\rightarrow B(y))$ ($t$ is again some arbitrary term), and then use $A(d)$ to deduce $B(t)$.
A: Let's be absolutely clear. In a standard Natural Deduction system you can only "get rid of" -- better, instantiate -- one quantifier at a time (the outermost, initial one). However, from 
$$\forall y\big(A(x)\to B(y)\big)$$
you can infer e.g.
$$ \forall y\big(A(d)\to B(y)\big)$$
And now you can use the universal quantifier instantiation rule again, and again -- just as in the first case -- that rule allows you to instantiate with any constant, so you can use $d$ again, to get
$$\big(A(d)\to B(d)\big).$$
A: Couldn't you just get rid of the quantifiers with $A(d) \to B(d)$ as well?  I mean, it's true for ALL $x$ and $y$... but presumably $A(c)$ and $A(d)$ are different, so you couldn't just use what you wrote.  Luckily your initial premise is very, very flexible!
