Metamath Proof Explorer


Syntax definition ctanh

Description: Extend class notation to include the hyperbolic tangent function, see df-tanh .

Ref Expression
Assertion ctanh
class tanh