Syntax Definition wid4oa 27

Description: If a, b, c, and d are terms, so is (a == c, d ==OA b).

Hypotheses

Ref	Expression
wva	term a
wvb	term b
wvc	term c
wvd	term d

Assertion

Ref	Expression
wid4oa	term (a == c, d ==OA b)

See definition df-id4oa 57 for more information.

metamath.org