Is there a way of making the notion of "stronger theorem" precise? Mathematicians frequently speak of a theorem being stronger than another. But on its face, this does not make sense, since all theorems in a formal system imply each other, hence are equivalent. Is there some paper or text where this notion is made precise, where there is defined a preorder on theorems that is stronger than equivalence but weaker than strict identity? I would like a link to such a paper.
 A: "All theorems in a formal system imply each other". 
Not so.
Suppose $T \vdash_S A$ and $T \vdash_S B$ where $T$ is some theory whose deductive apparatus is $S$ [e.g. first-order logic], and $\vdash_S$ is syntactic entailment in $S$. Nothing whatsoever follows about whether $A \vdash_S B$ or $B \vdash_S A$. So the claim doesn't apply to theoremhood and implication understood in terms syntactic entailment.
Suppose $T \vDash_L A$ and $T \vDash_L B$ where $T$ is some theory in language $L$, and $\vDash_L$ is the notion of semantical entailment appropriate to the language $L$. Nothing whatsoever follows about whether $A \vDash_L B$ or $B \vDash_L A$. So the claim doesn't apply to theorem hood and implication understood in terms of semantic entailment either.
(Perhaps you think "implies"  in the sense relevant to talk about one theorem implying more than another is well captured by material implication, i.e. the truth-functional conditional. Well, it isn't. And anyway even if $T \supset A$ and $T \supset B$, nothing as yet follows about whether $A \supset B$ or $B \supset A$ either.)
A: Yes, there is a way of making this notion precise.  Namely, for two theorems $A$ and $B$ of a theory $T$, one can fix a subtheory $T_0$ of $T$ and ask whether or not $T_0 \cup \{A\} \vdash B$.  The idea is that the "base theory" $T_0$ has only some basic axioms that we take for granted (and which axioms we wish to take for granted can depend on the context.)
For example, both the Boolean Prime Ideal Theorem and the Hahn–Banach Theorem are provable in $\mathsf{ZFC}$; however, it is often said that 
the Hahn–Banach Theorem is weaker than the Boolean Prime Ideal Theorem because it can be proved from the $\mathsf{ZF}$ axioms plus the Boolean Prime Ideal Theorem, whereas the Boolean Prime Ideal Theorem cannot be proved from the $\mathsf{ZF}$ axioms plus the Hahn–Banach Theorem.
Naturally, the meaning of "weaker than" depends on the base theory (here it is $\mathsf{ZF}$.)
Besides consequences of $\mathsf{AC}$, another context in which this notion has been studied extensively is subsystems of second order arithmetic — see the book by Stephen G. Simpson by this name.  Here the theory $T$ is second-order arithmetic (instead of $\mathsf{ZFC}$) and the base theory $T_0$ is a weak subtheory called $\mathsf{RCA}_0$.
