Theorem tanhaddd

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

	Ref	Expression
Hypotheses	tanhaddd.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	tanhaddd.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
	tanhaddd.1	⊢ ( 𝜑 → ( cosh ‘ 𝐴 ) ≠ 0 )
	tanhaddd.2	⊢ ( 𝜑 → ( cosh ‘ 𝐵 ) ≠ 0 )
	tanhaddd.3	⊢ ( 𝜑 → ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 )
Assertion	tanhaddd	⊢ ( 𝜑 → ( tanh ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( tanh ‘ 𝐴 ) + ( tanh ‘ 𝐵 ) ) / ( 1 + ( ( tanh ‘ 𝐴 ) · ( tanh ‘ 𝐵 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		tanhaddd.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		tanhaddd.b	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
3		tanhaddd.1	⊢ ( 𝜑 → ( cosh ‘ 𝐴 ) ≠ 0 )
4		tanhaddd.2	⊢ ( 𝜑 → ( cosh ‘ 𝐵 ) ≠ 0 )
5		tanhaddd.3	⊢ ( 𝜑 → ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 )
6	1 2	jca	⊢ ( 𝜑 → ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) )
7		tanhadd	⊢ ( ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ ( cosh ‘ 𝐴 ) ≠ 0 ) ∧ ( ( cosh ‘ 𝐵 ) ≠ 0 ∧ ( cosh ‘ ( 𝐴 + 𝐵 ) ) ≠ 0 ) ) → ( tanh ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( tanh ‘ 𝐴 ) + ( tanh ‘ 𝐵 ) ) / ( 1 + ( ( tanh ‘ 𝐴 ) · ( tanh ‘ 𝐵 ) ) ) ) )
8	6 3 4 5 7	syl22anc	⊢ ( 𝜑 → ( tanh ‘ ( 𝐴 + 𝐵 ) ) = ( ( ( tanh ‘ 𝐴 ) + ( tanh ‘ 𝐵 ) ) / ( 1 + ( ( tanh ‘ 𝐴 ) · ( tanh ‘ 𝐵 ) ) ) ) )