  This paper is part of the general project of proof mining, developed by
Kohlenbach. By "proof mining" we mean the logical analysis of mathematical
proofs with the aim of extracting new numerically relevant information hidden
in the proofs.
  We present logical metatheorems for classes of spaces from functional
analysis and hyperbolic geometry, like Gromov hyperbolic spaces, ${\mathbb
R}$-trees and uniformly convex hyperbolic spaces. Our theorems are adaptations
to these structures of previous metatheorems of Gerhardy and Kohlenbach, and
they guarantee a-priori, under very general logical conditions, the existence
of uniform bounds.
  We give also an application in nonlinear functional analysis, more
specifically in metric fixed-point theory. Thus, we show that the uniform bound
on the rate of asymptotic regularity for the Krasnoselski-Mann iterations of
nonexpansive mappings in uniformly convex hyperbolic spaces obtained in a
previous paper is an instance of one of our metatheorems.
