Is there a database for tracking the dependencies of mathematical theorems? Given a proof for a result, one could denote the proof as a node on a graph, and then draw arrows to the node from axioms and previous results that the proof uses, and then draw arrows from the node to results that the result is used to prove. The sources of such a graph would be mathematical axioms and the sinks would be results which do not yet have corollaries. This is related to the facts that finite categories can be drawn as directed graphs and that proofs form a category.
Question: Is there an existing ontological/relational database somewhere that attempts to make use of such an idea to formally encode some of present-day mathematics?
It can often be difficult to fully trace all of the logical dependencies of a given result. For example, how can one show whether existing proofs of the Implicit Function Theorem use the Law of the Excluded Middle or not? Rather than spend a couple of days going through tens of textbooks and trying to parse their proofs, not for their content but just to see what assumptions they are using, wouldn't it be easier to ask a computer to do that task? 
Such a system for tracking the logical dependencies of known proofs for existing theorems could be useful not only for beginners ("What important theorems use the completeness property of the real numbers? I'll check the database."), but it could also be useful for constructivists or intuitionists who want to keep track of which existing results make use of the Axiom of Choice or the Law of the Excluded Middle. And maybe it would be possible to use a sufficiently complete database to run tests to see whether the foundations of mathematics are consistent? I don't actually know, but it sounds on a naive level something that would be useful, even if it would take a long time to build.
Note: I am not sure what to tag this question or if it is on-topic.
 A: While the other answers given are quite good, there are a few other issues I would bring up.
(1) How do we avoid bogging the system down with irrelevant pieces of mathematics?
(2) Which axiomatic system do we use?  If we use ZFC, there are in fact infinitely many axioms.  Moreover, proving some well-known results can be quite messy when viewing things using the language of set theory, or even in some native theory.  (For instance, look at how long it took to formalize the Feit-Thompson theorem in Coq!)
On the other hand, if we use multiple languages/axiomatic systems, we run into the fact that there are no sinks.  For any axiom A in one system, there is another axiom B in another system, which can be proved equivalent using axioms from a third system!  We then get into reverse mathematics, which is quite interesting, but also (rightly) limited to certain key theorems and their equivalences.
A: The reverse mathematics zoo, founded by Damir Dzhafarov and with recent development by Eric Astor, aims to be a database showing the relations and dependencies of mathematical theorems as described in the theory of reverse mathematics. An enormous number of the theorems of classical mathematics are now included in the reverse mathematical hierarchy, and appear in this database. 
The system accepts new contributions, and is capable of generating diagrams showing the relations. 
For example, the current results.txt file and the database is available in the rmzoo.zip file.  There are various diagrams available http://rmzoo.math.uconn.edu/diagrams/, which are generated automatically from the database. 
Pictured here is the Implications and Strict Implications diagram.

A: It's important to distinguish between two types of "dependencies."
The cleanest type of dependency is the kind that is studied in reverse mathematics: Theorem T depends on Axiom A if T is actually unprovable in the absence of A.  Folks who study reverse mathematics make it their job to track dependencies of this type.  Proof assistants such as Coq also allow you to track some such dependencies; for example, Coq doesn't have the law of the excluded middle built in, so you can definitively confirm (in some cases) that some theorem does not need the law of the excluded middle.  So if this is the kind of dependency you're interested in, then there are people who are working hard on tracking it (but a complete database of the sort you're looking for isn't quite available yet).
There is another type of dependency that is less formal.  An example might be "The only known proof of Theorem T relies on the classification of finite simple groups (CFSG)."  We understand intuitively what this means, but it is difficult to formalize.  CFSG is not an axiom, and we don't know any plausible way to formalize "a system of mathematics in which CFSG is unprovable but lots of other mathematics is provable."  Thus the best we could do is to provide the computer with all known proofs and then it could verify that every known proof of T uses CFSG as a lemma.  This is a much more ambitious task than formalizing at least one proof of every mathematical theorem, and even the latter project is at least decades away.  For now, human expert knowledge is a better guide to this sort of thing than computers are.
A: The Stacks Project provides an example of what you're looking for.  Every definition, lemma, theorem, etc. is given a tag, and the tags are used as references in proofs.  They even provide an API for visualizing the tag graph using d3.js.  Of course the scope of the project is limited to algebraic geometry and related topics, and I'm not sure whether or not they drill all the way down to axioms of set theory, but it's a pretty good start.
A: Not an answer, just
a diagram from the Stacks Project, mentioned by Paul Siegel,
illustrating dependencies of "the results needed to prove Chow’s Lemma" (the Noetherian case):

     


          

(Image from MathBabe blog.)


And here's a link to a larger image.
