Double negation elimination

holds. It asserts that if it is false that $A$ is false, then $A$ is true.

$$\neg\neg A \to A$$

Remark. Classical logic accepts this. Intuitionistic/Constructive logic rejects it: showing that $\neg A$ leads to contradiction is not the same as constructing a proof of $A$. You have ruled something out, but you have not built the required Witness.