ThmDex – An index of mathematical definitions, results, and conjectures.
P3585
Define $g(x) : = - x^2 / 2$. From result R5265: Slope function for real monomial function of one variable, we know that $g'(x) = - x$.

Using results
(i) R5256: Slope function for composition of two differentiable real functions
(ii) R5254: Slope function for standard natural real exponential function

we now have \begin{equation} \begin{split} \frac{d f(x)}{d x} & = \frac{1}{\sqrt{2 \pi}} \frac{d \exp(g(x))}{d g(x)} \frac{d g(x)}{d x} \\ & = \frac{1}{\sqrt{2 \pi}} \exp(g(x)) \frac{d g(x)}{d x} \\ & = f(x) \frac{d g(x)}{d x} \\ & = - x f(x) \\ \end{split} \end{equation} $\square$