Commuting symmetric matrices have a common orthonormal eigenbasis

For commuting real symmetric matrices $A,B$, each eigenspace of $A$ is invariant under $B$: $A(Bv)=B(Av)=\lambda Bv$. The restriction of $B$ to that eigenspace is again symmetric. The spectral theorem therefore supplies an orthonormal eigenbasis for $B$ inside each eigenspace of $A$. Combining these bases gives a common orthonormal eigenbasis of the whole space. Conversely, two symmetric matrices diagonal in the same orthonormal basis commute.