Syntax Definition wid3oa 27

Description: If a, b, and c are terms, so is (a ≡ c ≡_OA b).

Hypotheses

Ref	Expression
wva	term  a
wvb	term  b
wvc	term  c

Assertion

Ref	Expression
wid3oa	term  (a ≡ c ≡OA b)

See definition df-id3oa 57 for more information.