Syntax Definition wle2 11

Description: If a and b are terms, so is (a =<2 b).

Hypotheses

Ref	Expression
wva	term a
wvb	term b

Assertion

Ref	Expression
wle2	term (a =<2 b)

See definition df-le 121 for more information.

metamath.org