wff-bi - bfol.mm Proof Explorer

	bfol.mm Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > PE Home > Th. List > wff-bi

Syntax Definition wff-bi 104

Description: Extend WFF definition to include the biconditional symbol '↔'.

**Hypotheses**
Ref	Expression
wff-ph	wff 𝜑
wff-ps	wff 𝜓

**Assertion**
Ref	Expression
wff-bi	wff (𝜑 ↔ 𝜓)

See definition df-bi-D2.1 107 for more information.

Colors of variables: wff objvar term class