One consequence of Shoenfield's theorem relates to the axiom of choice. Gödel proved that the constructible universe "L" always satisfies ZFC, including the axiom of choice, even when "V" is only assumed to satisfy ZF. Shoenfield's theorem shows that if there is a model of ZF in which a given formula_3 statement φ is false, then φ is also false in the constructible universe of that model. In contrapositive, this means that if ZFC proves a formula_3 sentence then that sentence is also provable in ZF. The same argument can be applied to any other principle which always holds in the constructible universe, such as the combinatorial principle ◊. Even if these principles are independent of ZF, each of their formula_3 consequences is already provable in ZF. In particular, this includes any of their consequences that can be expressed in the (first order) language of Peano arithmetic.