wff-true - bfol.mm Proof Explorer

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

Syntax Definition wff-true 153

Description: Extend WFF definition to include the "true" constant '⊤'.

**Assertion**
Ref	Expression
wff-true	wff ⊤

See definition df-true-D2.4 155 for more information.

Colors of variables: wff objvar term class