let th1, th2, th3 be Real; ( cos th1 <> 0 & cos th2 <> 0 & cos th3 <> 0 implies tan ((th1 + th2) + th3) = ((((tan th1) + (tan th2)) + (tan th3)) - (((tan th1) * (tan th2)) * (tan th3))) / (((1 - ((tan th2) * (tan th3))) - ((tan th3) * (tan th1))) - ((tan th1) * (tan th2))) )
assume that
A1:
( cos th1 <> 0 & cos th2 <> 0 )
and
A2:
cos th3 <> 0
; tan ((th1 + th2) + th3) = ((((tan th1) + (tan th2)) + (tan th3)) - (((tan th1) * (tan th2)) * (tan th3))) / (((1 - ((tan th2) * (tan th3))) - ((tan th3) * (tan th1))) - ((tan th1) * (tan th2)))
A3:
(cos th1) * (cos th2) <> 0
by A1;
tan ((th1 + th2) + th3) =
((((cos th1) * (cos th2)) * (cos th3)) * ((((tan th1) + (tan th2)) + (tan th3)) - (((tan th1) * (tan th2)) * (tan th3)))) / (cos ((th1 + th2) + th3))
by A1, A2, Th11
.=
((((cos th1) * (cos th2)) * (cos th3)) * ((((tan th1) + (tan th2)) + (tan th3)) - (((tan th1) * (tan th2)) * (tan th3)))) / ((((cos th1) * (cos th2)) * (cos th3)) * (((1 - ((tan th2) * (tan th3))) - ((tan th3) * (tan th1))) - ((tan th1) * (tan th2))))
by A1, A2, Th12
.=
((((cos th1) * (cos th2)) * (cos th3)) / (((cos th1) * (cos th2)) * (cos th3))) / ((((1 - ((tan th2) * (tan th3))) - ((tan th3) * (tan th1))) - ((tan th1) * (tan th2))) / ((((tan th1) + (tan th2)) + (tan th3)) - (((tan th1) * (tan th2)) * (tan th3))))
by XCMPLX_1:84
.=
1 / ((((1 - ((tan th2) * (tan th3))) - ((tan th3) * (tan th1))) - ((tan th1) * (tan th2))) / ((((tan th1) + (tan th2)) + (tan th3)) - (((tan th1) * (tan th2)) * (tan th3))))
by A2, A3, XCMPLX_1:60
.=
((((tan th1) + (tan th2)) + (tan th3)) - (((tan th1) * (tan th2)) * (tan th3))) / (((1 - ((tan th2) * (tan th3))) - ((tan th3) * (tan th1))) - ((tan th1) * (tan th2)))
by XCMPLX_1:57
;
hence
tan ((th1 + th2) + th3) = ((((tan th1) + (tan th2)) + (tan th3)) - (((tan th1) * (tan th2)) * (tan th3))) / (((1 - ((tan th2) * (tan th3))) - ((tan th3) * (tan th1))) - ((tan th1) * (tan th2)))
; verum