This property is called "coherence", and no, it doesn't always hold.
Establishing this property holds for a given semantics of proofs is a proof obligation. An example of when it doesn't arises with coercive subtyping -- if the diagrams corresponding to possible coercions do not all commute, then the semantics is not coherent, in that the meaning of a term depends critically on its typing derivation. If all you have is the term and knowledge that it has a typing derivation, you can't tell what it means, necessarily.
For a proof-theoretic characterization, the thing to look for is a cut-elimination theorem. One way of reading the cut-elimination theorem is precisely that it says that eliminating intro/elim and elim/intro pairs (i.e., $\beta$ and $\eta$ equations) induces a genuine equivalence relation on proofs.
However, we can still have essentially different proofs. For example, $x : A \land A \vdash \pi_1(x) : A$ and $x : A \land A \vdash \pi_2(x) : A$ are two different proofs that $A$ and $A$ entails $A$. However, cut-elimination guarantees that the addition of proof terms does make the typing derivations unique -- any proof of this entailment must be equal to one or the other, since every proof is equivalent to a cut-free proof, and these are the only two cut-free proofs, and the proof terms let us distinguish the two possibilities.
EDIT: There must be a treatment of this subject in somebody's book (Barendregt?), but I don't know off-hand, since I learned it via osmosis. Probably the best reference I can point you at is Jan Schwinghammer's paper "Coherence of Subsumption for Monadic Types", which nicely illustrates the idea, and whose references also contain pointers to the best available literature.
Noam quite rightly points out that you might actually be interested in the case where all derivations of a judgement are equivalent. (This possibility honestly hadn't even occurred to me, since I'm too intuitionistically contaminated.) The keyword to search for in this case is "proof irrelevance", and I recommend Awodey and Bauer's paper "Propositions as [Types]".
EDIT 2: When cut-elimination holds, then the derivations of a calculus with proof terms become equivalent. If you don't have proof terms, then you can't guarantee equivalence of derivations.
For example, suppose we erased the proof terms from the derivation above, so that we simply had the judgment $A \land A \vdash A$. In this case, even if we know that this judgment holds, we still don't know whether the proof used the left or the right $A$, which are the two intrinsically different derivations of the same judgment. On the other hand, if we have proof terms, then we have a judgment $x : A \land A \vdash e : A$. In this case, the derivation does bebgcome unique, because now we can $\beta\eta$-normalize $e$ and just check whether it is equal to $\pi_1(x)$ or $\pi_2(x)$.
This is why lambda-calculus expressions are called "proof terms": these terms are evidence to establish which proof you meant.
To connect this back with proof irrelevance, a type is "proof irrelevant" when all the proof terms of that type are equivalent. That is, if $\Gamma \vdash e : A$ and $\Gamma \vdash e' : A$, then we know that the two derivations are equivalent, regardless of $e$ and $e'$. For example, the unit type $1$ is proof irrelevant, since every term in it is equivalent to the unit value $\left<\right>$.
