theorem :: SIN_COS4:35

for th1, th2, th3 being Real holds ((sin th1) * (cos th2)) * (cos th3) = (1 / 4) * ((((sin ((th1 + th2) - th3)) - (sin ((th2 + th3) - th1))) + (sin ((th3 + th1) - th2))) + (sin ((th1 + th2) + th3)))