If every mathematical theorem can be derived from the ZFC axioms, and the ZFC axioms can be derived from symbolic logic (can they? Is that roughly what Principia Mathematica attempts to do?), then why do we still use the ZFC axioms?
Godel's theorem seems to say that a formal system can't prove itself true. But in what sense does this undermine the logicist program? Isn't it still best to use the simplest axioms possible, and the axioms of logic are simpler than the axioms of ZFC?
On
The usual summary of the program of "logicism" - which Principia Mathematica was key part of - was that it wanted to show that all of mathematics could be developed from logic alone. However, this program is now usually viewed as unsuccessful. Of course, nothing is philosophy has a unanimous viewpoint - there are always some people on any side of any argument - but the SEP article on logicism has an entire section of "Summary of Problems for Logicism" which describes 11 significant concerns with the program. I think it is fair to say that few people working in logic today feel that the ZFC axioms can be reduced purely to logic. Peter Smith's answer says more about this.
What I would like to answer is the question "Isn't it still best to use the simplest axioms possible...?". The usual answer today is: sure, but it is not best to use axioms that are more simple than possible.
The idea of a single foundational set of axioms, which all of mathematics could be reduced to, was a common discussion point in the early history of mathematical logic. Many logicians now view that idea as too simple. Based on our experience with logicism, with the incompleteness theorems, and with the general art of formalizing mathematics, we now see that there are many formal systems, each of which has its own place. (In this sense, so to speak, logic has moved forward from objective, Enlightenment-style thinking towards a viewpoint more friendly towards subjective viewpoints, just as many other fields of study have.)
For certain kinds of questions, the axioms of Peano arithmetic are the most natural place to start. For other mathematical questions, ZF or ZFC is the natural place to be. In between these, we have second-order arithmetic and its subsystems. Above them, in a sense, we have ZF or ZFC combined with large cardinal axioms or determinacy axioms. To the side, we have constructive theories that do not use classical logic. To another side, we have axiom systems based on topos theory.
Each of these different logical systems has a place for studying particular kinds of mathematical questions. The goal of reducing everything to a single "best" system was a dream from a previous era, but we now see that things are much more complicated - and more interesting - than that goal could accommodate.
"[If] every mathematical theorem can be derived from the ZFC axioms ...". Well not so. Yes, we can reconstruct large chunks of familiar maths in ZFC. But even lots of set theorists work with "large cardinal" axioms which are unprovable in ZFC. And e.g. category theorists make assumptions that go beyond what we can construct in ZFC.
"...and the ZFC axioms can be derived from symbolic logic". No, they can't be. ZFC asserts the existence of an infinity of sets, surprise, surprise. The most that standard logic asserts is the existence of at least one object (and perhaps it shouldn't do even that, but let's not worry about that wrinkle). So ZFC can't possibly be derived from symbolic logic alone. It is a formalizable theory which, when formalized, uses a formalized symbolic logic as its deductive apparatus; but the axioms of ZFC are not themselves propositions of logic.
"Is that roughly what Principia Mathematica attempts to do?" How "rough" do we want to be? Principia isn't a set theory: it is a no-class theory that tries to do what set theories do without sets (but with something called propositional functions instead). And Principia, by most reckonings, goes beyond pure logic, by making strong existence assumptions --it has an Axiom of Infinity that tells us that there are infinitely many things (which is not a claim of pure logic by most people's standards, arguably not even by Russell and Whitehead's).
"Godel's theorem seems to say that a formal system can't prove itself true." No it doesn't. The Gödelian theorems don't talk about truth (semantics) but about provability (syntax). The second incompleteness theorem "says" (in a stretched sense) that a suitably strong formal system can't prove that "$0 = 1$" is unprovable in the system.
If you are interested in these foundational matters you need to do some more homework. Try e.g. Marcus Giaquinto's terrific (and terrifically clear) The Search for Certainty which you should find very illuminating about the general issues you touch on.