Solution (source code)

= Solution

Apply the <vector triple product identity> $p\times(c\times d)=c(p\cdot d)-d(p\cdot c)$ with $p=a\times b$. This gives
$$
(a\times b)\times(c\times d)
=c\big((a\times b)\cdot d\big)-d\big((a\times b)\cdot c\big).
$$
For column <vectors> $a,b,d$, the <scalar triple product> is $(a\times b)\cdot d=\det(a,b,d)$; replacing $d$ by $c$ gives the other coefficient. Therefore
$$
\boxed{(a\times b)\times(c\times d)=\det(a,b,d)c-\det(a,b,c)d.}
$$
The signs follow the stated column convention and the cyclic invariance of the <scalar triple product>. No independence assumptions on the four <vectors> are needed.