wff-or - bfol.mm Proof Explorer

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

Syntax Definition wff-or 144

Description: Extend WFF definition to include the "or" symbol '∨'.

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

**Assertion**
Ref	Expression
wff-or	wff (𝜑 ∨ 𝜓)

See definition df-or-D2.3 145 for more information.

Colors of variables: wff objvar term class