The difference between $\beta$-reduction and $let$
In the untyped lambda calculus, $\mathsf{let}$ is indeed useless, and most presentations leave it out. But in many typed lambda calculi, $\mathsf{let}$ is useful because it has a more general typing rule.
The best known example is the Hindley-Milner type system, which derives its power from let-polymorphism. In $(\lambda x.e_1) \: e_2$, the expression $e_1$ has one particular type, which is also the type of $x$ when typing $e_1$. But in $\mathsf{let} \: x = e_1 \: \mathsf{in} \: e_2$, $e_1$ can be polymorphic, and the instances of $x$ in $e_1$ can have different specializations of this polymorphic type.