Deriving BAC-CAB from differential forms
I know that this question already has an accepted answer, but let me give an answer from a purist differential forms perspective. Recall that if $V$ is an $n$-dimensional inner product space, then the Hodge star is a linear isomorphism $\ast : \bigwedge^k V \to \bigwedge^{n-k} V$ for each $0 \leq k \leq n$, satisfying the following:
for $v$, $w \in V$, $\langle v,w\rangle \omega = v \wedge \ast w$ for $\omega = \ast 1$ the generator of $\bigwedge^n V$ satisfying $\omega = e_1 \wedge \cdots \wedge e_n$ for any orthonormal basis $\{e_k\}$ of $V$ with the appropriate orientation (e.g., the volume form in $\bigwedge^n (\mathbb{R}^n)^\ast$);
in particular, $\ast \ast = \operatorname{Id}$ when $n$ is odd.
Also, recall that the inner product on $\bigwedge^k V$ is given by $$ \langle v_1 \wedge \cdots \wedge v_k, w_1 \wedge \cdots \wedge w_k \rangle = \det(\langle v_i,w_j \rangle). $$
So, suppose that $V$ is $3$-dimensional, in which case we can define the cross product of $a$, $b \in V$ by $$ a \times b := \ast (a \wedge b). $$ Let $u$, $v$, $w \in V$. Then for any $x \in V$, $$ \langle u \times (v \times w), x \rangle \omega = \langle x, u \times (v \times w) \rangle \omega\\ = \langle x, \ast (u \wedge \ast(v \wedge w)) \rangle \omega\\ = x \wedge \ast \ast (u \wedge \ast(v \wedge w))\\ = x \wedge (u \wedge \ast(v \wedge w))\\ = (x \wedge u) \wedge \ast (v \wedge w)\\ = \langle x \wedge u, v \wedge w \rangle \omega\\ = (\langle x,v \rangle\langle u,w \rangle - \langle x,w \rangle\langle u,v \rangle)\omega\\ = \langle \langle u,w \rangle v - \langle u,v \rangle w, x \rangle \omega, $$ implying that $$ \langle u \times (v \times w), x \rangle = \langle \langle u,w \rangle v - \langle u,v \rangle w, x \rangle, $$ and hence, since $x$ was arbitrary, that $$ u \times (v \times w) = \langle u,w \rangle v - \langle u,v \rangle w, $$ as required.
Proving identities with geometric algebra (which subsumes differential forms):
Let $\langle A \rangle_n$ denote the grade-$n$ projection of a multivector $A$. For example, let $A = a + b \wedge c + d \wedge e \wedge f$. Then the grade-2 project is $\langle A \rangle_2 = a \wedge b$.
What geometric algebra has that differential forms does not is the geometric product, which marries the dot and wedge products. On two vectors $a$, $b$, the geometric product takes the form $ab$, which is
$$ab \equiv a \cdot b + a \wedge b$$
Like the wedge product, the geometric product is associative, but the vectors neither strictlly commute nor strictly anticommute in general.
We handle the Hodge dual by geometric product multiplication by the pseudoscalar $i = \hat x \wedge \hat y \wedge \hat z$. That is,
$$\star a = ia$$
For any vector $a$.
Using grade projection and the geometric product, it is quite easy to prove some of these identities. To prove the BAC-CAB rule, take $\langle abc \rangle_1$.
$$\langle a(bc) \rangle_1 = a \cdot (b \wedge c) + a (b \cdot c)$$
This groups the $(bc)$ vectors together. (nb. the "dot" product of a vector and a bivector is a vector. $a \cdot (b \wedge c)$ is a vector lying in the plane $b \wedge c$ orthogonal to $a$). But by associativity, we can group the $(ab)$ vectors together.
$$\langle (ab)c \rangle_1 = (b \cdot a) c + (a \wedge b) \cdot c$$
Since $(ab)c = a(bc)$, this generates an equation looking like
$$a \cdot (b \wedge c) + a(b \cdot c) = c(a \cdot b) + (a \wedge b) \cdot c$$
So we have the CAB part, but not the BAC part. Notice we have $a (b \cdot c)$ that we want to cancel. To do this, let's try $bca$.
$$\begin{align*} \langle bca \rangle_1 &= a(b \cdot c) + (b \wedge c) \cdot a \\ &= b (a \cdot c) + b \cdot (c \wedge a)\end{align*}$$
We can use this to subtract the top equation from the left and the bottom from the right to get:
$$2a \cdot (b \wedge c) = c (a \cdot b) - b(a \cdot c) + (a \wedge b) \cdot c - b \cdot (c \wedge a)$$
Not done yet. Let's look at one more expansion, of $cab$.
$$\begin{align*} \langle cab \rangle_1 &= (c \cdot a)b + (c \wedge a) \cdot b \\ &= c(a \cdot b) + c \cdot (a \wedge b)\end{align*}$$
Put all of these on one side of an equals sign, and you can cancel out the terms we don't want, yielding
$$2a \cdot (b \wedge c) = 2c(a \cdot b) - 2 b(a \cdot c)$$
This is the proper form of the BAC-CAB rule (within a factor of 2). The usual form can be recovered by $b \wedge c = i (b \times c)$.
Honestly, doing it this way is pretty onerous. I've done it several times, and breaking it down into components is a lot less tedious. One of the few times I've found that to be the case. Nevertheless, using associativity of the geometric product and grade projection is something I rely on heavily to derive useful identities or simplify expressions. It's just a pity that traditional differential forms lacks these very useful tools from clifford algebra.