Syntax Definition w3o 580

Description: Extend wff definition to include 3-way disjunction ('or').

Hypotheses

Ref	Expression
wph	wff φ
wps	wff ψ
wch	wff χ

Assertion

Ref	Expression
w3o	wff (φ ∨ ψ ∨ χ)

See definition df-3or 582 for more information.

metamath.org