Worked solution: Independence of Suslin's Hypothesis from ZFC (Jensen, Solovay–Tennenbaum, 1971)

Combining the two halves: relative to $\mathrm{Con}(\mathrm{ZFC})$, both $\mathrm{ZFC} + \neg\mathrm{SH}$ (Jensen 1968 via $\diamondsuit$; Jech 1967 and Tennenbaum 1968 via direct forcing) and $\mathrm{ZFC} + \mathrm{SH}$ (Solovay–Tennenbaum 1971 via iterated forcing, since $\mathrm{MA} + \neg\mathrm{CH}$ implies $\mathrm{SH}$) are consistent theories, so Suslin's Hypothesis is formally undecidable from $\mathrm{ZFC}$ alone.

Neither half was dispensable: Jensen's and Jech/Tennenbaum's constructions only show $\mathrm{SH}$ cannot be proved from $\mathrm{ZFC}$; without the Solovay–Tennenbaum half, it would remain conceivable that $\mathrm{SH}$'s negation could itself be a theorem of $\mathrm{ZFC}$, in the same way that Gödel's construction of $L$ alone left CH's provability open until Cohen's forcing closed the gap. It took a fundamentally new technique — long iterated forcing, rather than a single forcing step or a fixed inner model — to build the second half, illustrating that some independence results demand real innovation on both sides.

Suslin's Hypothesis is also historically significant as one of the first "ordinary" mathematical statements about the real line and general topology, rather than a statement directly about sets or cardinal arithmetic, shown independent of $\mathrm{ZFC}$ — foreshadowing that even classical questions in analysis, topology, and (as the next proof preset shows) algebra could hide genuine set-theoretic content.