Does one proof imply the existence of other proofs?

I think this is an example of the sort of the thing you're looking for:

Any sentence of number theory that can be proven using the axiom of choice and/or the continuum hypothesis can be proven from ZF alone, without using the axiom of choice or the continuum hypothesis.

In other words, if there is a proof of a sentence of number theory that uses AC and/or CH, then you can find some other proof of the sentence that doesn't use AC or CH.

A sentence of number theory here is a first-order statement about the structure $\langle \mathbb{N}; +, \cdot; \le\rangle.$ This is a statement about the natural numbers under the usual arithmetic operations and the usual ordering, where all quantifiers are over the natural numbers.

This is called a sentence of number theory because it's the kind of statement that is normally considered part of number theory (rather than, say, analysis). Here are some examples of sentences of number theory:

  1. Fermat's last theorem: There do not exist positive integers $x, y, z,$ and $n$ such that $n\ge 3$ and $x^n+y^n=z^n.$

  2. Goldbach's conjecture: Every even positive integer greater than $2$ can be written as the sum of two primes.

  3. The Collatz conjecture: If you start with any positive integer and generate a sequence by repeatedly taking the current number $n$ and either dividing it by $2$ (if $n$ is even) or computing $3n+1$ (if $n$ is odd), you'll eventually reach $1.$ (To see that this is a first-order statement as described above, you need to set up the machinery of coding finite sequences as individual numbers, but that can be done in a straightforward fashion.)

  4. P=NP.

  5. Even the Riemann hypothesis: As customarily written, this is not a sentence of number theory (it's about infinite series of complex numbers), but it is equivalent to a sentence of number theory. You can see this either by either talking about rational approximations of all the numbers involved or by using one of the number-theoretic equivalents that are known (which are arguably the reason that the Riemann hypothesis is of interest anyway).

If any of the sentences above can be proven using the axiom of choice and the continuum hypothesis, then they can actually be proven without those special assumptions.

None of the above sentences except 1 are known to be true. However, their negations are also sentences of number of theory, so it's also true that if any of 2-5 can be disproven using AC and/or CH, then they can be disproven without those special assumptions.

$$ $$

By the way, here are some examples of statements that are not sentences of number theory:

  1. There are uncountably many real numbers.

  2. The countable union of a countable set of real numbers is countable.

There's no way to express these without quantifying over real numbers, or, equivalently, over sets of natural numbers. (At least for example 7, even that's not sufficient; to express that, you need to quantify over sets of real numbers.)

$$ $$

The removability of AC and CH from the proof of any number-theoretic statement follows from the fact that Gödel's constructible universe $L,$ in which AC and CH are true, has the same natural numbers as the entire mathematical universe $V$ (along with the same addition, multiplication, and ordering).

This type of result can be extended considerably, by the way. First, it applies to the generalized continuum hypothesis, since that's true in $L.$ More interestingly, the Shoenfield absoluteness theorem shows that it also applies to some (but not all!) sentences of analysis; the sentences it applies to are allowed to include quantification over real numbers and/or sets of natural numbers, but the number of quantifier alternations is restricted.