Glivenko's Theorem

If $\phi$ is provable in classical logic, double negation inserted $\neg \neg \phi$ is provable in intuitionistic logic.

theorem iff_provable_dn_efq_dne_provable: 𝐈𝐧𝐭 ⊢! ~~p ↔ 𝐂𝐥 ⊢! p