Silver: if SCH holds at all singular strong limits of countable cofinality, SCH holds

Suppose the singular cardinals hypothesis holds at every singular strong limit cardinal of countable cofinality: for every singular strong limit cardinal $\lambda$ with $\operatorname{cf}\lambda=\aleph_0$,

Then the singular cardinals hypothesis holds at every singular strong limit cardinal $\kappa$, whatever its cofinality:

This is the consequence of Silver's theorem singled out in the source: failures of SCH can only first occur at cardinals of countable cofinality, which is why the consistency results for $\neg$SCH (Prikry forcing over a measurable cardinal) produce counterexamples such as $\aleph_\omega$.

Formalization Note SCH is the first (strong-limit) form, SingularCardinals.SCH. The analogous reduction for the second form is the published theorem JechSetTheory.sch_of_sch_cof_aleph0, included in this mission as a milestone.