Syntax Definition wb 127

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

Hypotheses

Ref	Expression
wph	wff φ
wps	wff ψ

Assertion

Ref	Expression
wb	wff (φ ↔ ψ)

See definition df-bi 128 for more information.

metamath.org