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	⊢ 𝜑
1		wps	⊢ 𝜓
2		wch	⊢ 𝜒
3	0 1 2	w3o	⊢ ( 𝜑 ∨ 𝜓 ∨ 𝜒 )
4	0 1	wo	⊢ ( 𝜑 ∨ 𝜓 )
5	4 2	wo	⊢ ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 )
6	3 5	wb	⊢ ( ( 𝜑 ∨ 𝜓 ∨ 𝜒 ) ↔ ( ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) )