Metamath Proof Explorer

Definition df-3or

Description: Define disjunction ('or') of three wff's. Definition *2.33 of WhiteheadRussell p. 105. This abbreviation reduces the number of parentheses and emphasizes that the order of bracketing is not important by virtue of the associative law orass . (Contributed by NM, 8-Apr-1994)

Ref Expression
Assertion df-3or φ ψ χ φ ψ χ

Detailed syntax breakdown

Step Hyp Ref Expression
0 wph wff φ
1 wps wff ψ
2 wch wff χ
3 0 1 2 w3o wff φ ψ χ
4 0 1 wo wff φ ψ
5 4 2 wo wff φ ψ χ
6 3 5 wb wff φ ψ χ φ ψ χ