Here is a braindead way to generate PBW theorems like this one:
One is given a presentation of an algebra, which allows one to put words in the generators $x_1,x_2,\dots,x_n$ into a "normal form" (in the case of the Clifford algebra, if $x_1,x_2,\dots,x_n$ is a basis of $V$, then a normal form might be words $x_{i_1} x_{i_2} \cdots x_{i_p}$ with $1 \leq i_1 < i_2 < \cdots < i_p \leq n$). One suspects that the set of words in normal form is actually a basis for the algebra. So one constructs the regular representation of the algebra in question. If the theorem is to be true, there is no choice about this: it is the vector space spanned by words in normal form, and the left (and right) multiplication operators are determined by the relations. Usually the easiest way to write down the formulas is recursively. One is then left to check that these operators satisfy the defining relations. This is "just linear algebra", but the computations in any particular example (or class of examples) may get messy. When it works, it usually works in arbitrary characteristic (and even integrally).
In the case of the Clifford algebra and similar algebras (e.g. enveloping algebras of Lie algebras, symplectic reflection algebras and their generalizations) this all works without too much difficulty. It also works for the Hecke algebra attached to a Coxeter system, though to make the calculations manageable in a case-free fashion it's good to use the Bourbaki trick of employing both the right and left representations simultaneously. There is even a general theorem here, which usually goes by the name "Bergman diamond lemma" (but in the cases I'd care most about, checking that its conditions are satisfied is just about the same level of difficulty as doing the work directly).
