Was there ever an axiom rendered a theorem? In the history of mathematics, are there notable examples of theorems which have been first considered axioms?
Alternatively, was there any statement first considered an axiom that later has been shown to be derived from other axiom(s), therefore rendering the statement a theorem?

Fraenkel introduced the axiom schema of replacement to set theory. This implied the axiom schema of comprehension, and allowed the empty set and unordered pair axioms to follow from the axiom of infinity. (Note Zermelo set theory includes the axiom of choice whereas ZF does not, so Zermelo+replacement is ZFC.) The "deleted" axioms are typically listed when describing ZF(C), partly so people realise they're in Zermelo set theory, partly for easier comparisons with other set theories of interest.
