theorem :: SIN_COS5:44

for x being Real holds cosh (3 * x) = (4 * ((cosh x) |^ 3)) - (3 * (cosh x))