Definition df-3or 935

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 510. (Contributed by NM, 8-Apr-1994.)

Assertion

Ref	Expression
df-3or	⊢ ((φ ∨ ψ ∨ χ) ↔ ((φ ∨ ψ) ∨ χ))

Detailed syntax breakdown of Definition df-3or

Step	Hyp	Ref	Expression
1		wph	. . 3 wff φ
2		wps	. . 3 wff ψ
3		wch	. . 3 wff χ
4	1, 2, 3	w3o 933	. 2 wff (φ ∨ ψ ∨ χ)
5	1, 2	wo 357	. . 3 wff (φ ∨ ψ)
6	5, 3	wo 357	. 2 wff ((φ ∨ ψ) ∨ χ)
7	4, 6	wb 176	1 wff ((φ ∨ ψ ∨ χ) ↔ ((φ ∨ ψ) ∨ χ))

This definition is referenced by:  3orass  937  3orrot  940  3anor  948  3ioran  950  3orbi123i  1141  3ori  1242  3jao  1243  3orbi123d  1251  3orim123d  1260  3or6  1263  cadan  1392  nf3or  1837  eueq3  3012  sspsstri  3372  eltpg  3770  rextpg  3779  ltfintrilem1  4466  sfin111  4537  nncdiv3lem2  6277  nncdiv3  6278