We show how to extract effective bounds $\Phi$ for $\bigwedge u^1 \bigwedge v \leq_\gamma tu \bigvee w^\eta G_0$-sentences which depend on $u$ only (i.e. $\bigwedge u \bigwedge v \leq_\gamma tu \bigvee w \leq_\eta \Phi uG_0$) from arithmetical proofs which use analytical assumptions of the form \begin{equation*}\tag{*}\bigwedge x^\delta\bigvee y \leq_\rho sx \bigwedge z^\tau F_0\end{equation*} $(\gamma, \delta, \rho$, and $\tau$ are arbitrary finite types, $\eta \leq 2, G_0$ and $F_0$ are quantifier-free, and $s$ and $t$ are closed terms). If $\tau \leq 2, (\ast)$ can be weakened to $\bigwedge x^\delta, z^\tau\bigvee y \leq_\rho sx \bigwedge \tilde{z} \leq_\tau z F_0$. This is used to establish new conservation results about weak Konig's lemma. Applications to proofs in classical analysis, especially uniqueness proofs in approximation theory, will be given in subsequent papers.