Syntax Definition wp 8

Description: If a and b are terms, so is (a^⊥ b).

Hypotheses

Ref	Expression
wva	term  a
wvb	term  b

Assertion

Ref	Expression
wp	term  (a⊥ b)

This syntax is primitive. The first axiom using it is ax-a4 32.

metamath.org