Metamath Proof Explorer


Syntax definition w3o

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

Ref Expression
Assertion w3o wff φ ψ χ