Let $M$ be a smooth manifold, let $h \in (0,h_0]$ be the semiclassical parameter, and fix a properly supported semiclassical pseudodifferential calculus on $M$ defined in local coordinate charts by left semiclassical quantization of symbols in $S^m(T^*M)$, with the standard coordinate-change invariance and local Euclidean composition formula for semiclassical left quantization. Let $\Psi_h^{-\infty}(M)$ denote the residual class consisting of smoothing operators whose Schwartz kernels are $O(h^N)$ in $C^\infty$ for every $N \in \mathbb N$. For each $m \in \mathbb R$, let \begin{align*} \sigma_h : \Psi_h^m(M) \to S^m(T^*M) /\bigl(hS^{m-1}(T^*M)+S^{-\infty}(T^*M)\bigr) \end{align*} be the corresponding semiclassical principal symbol map. If $m,m' \in \mathbb R$, $A \in \Psi_h^m(M)$ and $B \in \Psi_h^{m'}(M)$ are properly supported operators, then $AB$ is a properly supported element of $\Psi_h^{m+m'}(M)$, and \begin{align*} \sigma_h(AB)=\sigma_h(A)\sigma_h(B) \end{align*} in \begin{align*} S^{m+m'}(T^*M) /\bigl(hS^{m+m'-1}(T^*M)+S^{-\infty}(T^*M)\bigr). \end{align*}