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