theorem Th11: :: SIN_COS4:11

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