Syntax Definition wb 127

Description: Extend our wff definition to include the biconditional connective.

Hypotheses

Ref	Expression
wph	wff ph
wps	wff ps

Assertion

Ref	Expression
wb	wff (ph <-> ps)

See definition df-bi 128 for more information.

metamath.org