Syntax Definition wid4 22

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

Hypotheses

Ref	Expression
wva	term  a
wvb	term  b

Assertion

Ref	Expression
wid4	term  (a ≡4 b)

See definition df-id4 52 for more information.

metamath.org