wb - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Syntax Definition wb 146

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 147 for more information.

Colors of variables: wff set class