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.

Copyright terms: Public domain