Syntax Definition term-mult 5

Description: If '𝑡' and '𝑢' are terms, then '𝑡 ⋅ 𝑢' is a term.

Hypotheses

Ref	Expression
term-t	term 𝑡
term-u	term 𝑢

Assertion

Ref	Expression
term-mult	term (𝑡 ⋅ 𝑢)

This syntax is primitive. The first axiom using it is ax-L9-multl 25.