Theorem tanhaddd

Description: Addition formula for tanh. (Contributed by Jon Pennant, 9-Sep-2026)

	Ref	Expression
Hypotheses	tanhaddd.a	|- ( ph -> A e. CC )
	tanhaddd.b	|- ( ph -> B e. CC )
	tanhaddd.1	|- ( ph -> ( cosh ` A ) =/= 0 )
	tanhaddd.2	|- ( ph -> ( cosh ` B ) =/= 0 )
	tanhaddd.3	|- ( ph -> ( cosh ` ( A + B ) ) =/= 0 )
Assertion	tanhaddd	|- ( ph -> ( tanh ` ( A + B ) ) = ( ( ( tanh ` A ) + ( tanh ` B ) ) / ( 1 + ( ( tanh ` A ) x. ( tanh ` B ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		tanhaddd.a	|- ( ph -> A e. CC )
2		tanhaddd.b	|- ( ph -> B e. CC )
3		tanhaddd.1	|- ( ph -> ( cosh ` A ) =/= 0 )
4		tanhaddd.2	|- ( ph -> ( cosh ` B ) =/= 0 )
5		tanhaddd.3	|- ( ph -> ( cosh ` ( A + B ) ) =/= 0 )
6	1 2	jca	|- ( ph -> ( A e. CC /\ B e. CC ) )
7		tanhadd	|- ( ( ( ( A e. CC /\ B e. CC ) /\ ( cosh ` A ) =/= 0 ) /\ ( ( cosh ` B ) =/= 0 /\ ( cosh ` ( A + B ) ) =/= 0 ) ) -> ( tanh ` ( A + B ) ) = ( ( ( tanh ` A ) + ( tanh ` B ) ) / ( 1 + ( ( tanh ` A ) x. ( tanh ` B ) ) ) ) )
8	6 3 4 5 7	syl22anc	|- ( ph -> ( tanh ` ( A + B ) ) = ( ( ( tanh ` A ) + ( tanh ` B ) ) / ( 1 + ( ( tanh ` A ) x. ( tanh ` B ) ) ) ) )