theorem Th12: :: SIN_COS4:12

for th1, th2, th3 being Real st cos th1 <> 0 & cos th2 <> 0 & cos th3 <> 0 holds
cos ((th1 + th2) + th3) = (((cos th1) * (cos th2)) * (cos th3)) * (((1 - ((tan th2) * (tan th3))) - ((tan th3) * (tan th1))) - ((tan th1) * (tan th2)))