If I can prove $Y$ from "$X$ is true" and from "$X$ is false", can I prove $Y$ without using $X$ at all? Suppose I have a statement $X$, for which I do not know whether it is true or false. And suppose further that I want to prove a statement $Y$:

I first assume that $X$ is true, and I construct an involved argument that shows that $Y$ follows.
I then assume that $X$ is false, and another involved argument shows that $Y$ still follows.

I have then proven $Y$ (assuming excluded middle). Now, is there any kind of meta-theorem in mathematics that tells me that there should be a proof of $Y$ that is not mentioning $X$ at all (whatever that means formally)?
You can think about this as follows:

Was it necessary to have formulated $X$ in order to give a proof for $Y$, or could we have proven $Y$ right away without the &quot;halt in between&quot;?

For example, the Riemann hypothesis seems to be such an important &quot;halt in the middle&quot; for some statements.
I know, this is a rather informal question.
I do not want to formulate it in terms of mathematical logic and proof theory, simply beacuse I do not know enough about these subjects.
Maybe the question has a trivial counterexample if we go formal enough.
But then again, maybe someone with enough knowledge still sees an interesting variant of the question.
I am also happy to receive quite technical answers.
It is hard to say about what does a proof &quot;contains&quot; in here, indeed if $T∪\{a\}⊢x$ and $T∪\{¬a\}⊢x$ then $T⊢x$ because in any model of $T$ either $a$ or $¬a$ are true, hence $T⊨x⇒T⊢x$, but how do you define &quot;not mentioning&quot;?
One interpretation you can think of is if $a$ is not in the language of $T$, that is:
Given a theory $T$ in the language $\cal{L}$, and given a language $\cal{L}'\supset\cal{L}$, is it possible to have a formula $a$ in the language of $\cal{L}'$ such that $T∪\{a\}⊢_{\cal{L}'}x$ and $T∪\{¬a\}⊢_{\cal{L}'}x$ and $T⊢_{\cal{L}}x$ is false?
***In this interpretation the answer is false:
Let $\cal{L}$ be empty and $\{f,g\}=\cal{L}'$ be 1-ary functional symbols, and let $a$ be the following theory:
$$(f\text{ is injective}∧f\text{ is not surjective})∧(g\text{ is injective}∧g\text{ is surjective})$$
And let $x$ be:
$$∃z,y\ (z≠y)$$
Notice that $a$ does prove $x$, as well as $¬a$ proves $x$, but $x$ is not tautology.***
***As Noah said, this example is wrong, $¬a$ does not prove $x$.
Although the above answer is wrong, I leave this post up and not deleting it because it is yet another possible interpretation of the question.
Proposition: The set $c\mathbb R = \{cx : x\in\mathbb R\}$ is closed.
You can prove this if you assume $c=0,$ and also if you assume $c\ne0.$ But I will be surprised if you can do it without considering those two cases.