Summary: In the 1960s, mathematicians from Eastern Europe showed that every admissible rule in the intuitionistic implicational calculus is derivable. We prove the corresponding proposition for the simply typed lambda calculus: The type $μ_1 \to μ_2 \to \cdots μ_m \to v$ is inhabited iff for each substitution $s$ of types for the variables in $μ_1, \dots, μ_m$, $v$ the inhabitation of $s (μ_1), \dots, s(μ_m)$ implies the inhabitation of $s(v)$.