• Infix operator.
• x y is by default interpreted as DoubleLeftTee[x, y].
• x y z groups as (x y) z.
• Used in mathematics to indicate various strong forms of logical implication of x from y--often tautological implication.
• See Section 3.10.4 and Section 3.10.4.
• See also: \[LeftTee] , \[DoubleRightTee] .