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	$$⊢\left(\phi \vee \psi \vee \chi \right)\leftrightarrow \left(\left(\phi \vee \psi \right)\vee \chi \right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	$$wff\phi$$
1		wps	$$wff\psi$$
2		wch	$$wff\chi$$
3	0 1 2	w3o	$$wff\left(\phi \vee \psi \vee \chi \right)$$
4	0 1	wo	$$wff\left(\phi \vee \psi \right)$$
5	4 2	wo	$$wff\left(\left(\phi \vee \psi \right)\vee \chi \right)$$
6	3 5	wb	$$wff\left(\left(\phi \vee \psi \vee \chi \right)\leftrightarrow \left(\left(\phi \vee \psi \right)\vee \chi \right)\right)$$