Syntax Definition wb1 24

Description: If a and b are terms, so is (a <->3 b).

Hypotheses

Ref	Expression
wva	term a
wvb	term b

Assertion

Ref	Expression
wb1	term (a <->1 b)

See definition df-b1 1047 for more information.

Copyright terms: Public domain