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	|- ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	|- ph
1		wps	|- ps
2		wch	|- ch
3	0 1 2	w3o	|- ( ph \/ ps \/ ch )
4	0 1	wo	|- ( ph \/ ps )
5	4 2	wo	|- ( ( ph \/ ps ) \/ ch )
6	3 5	wb	|- ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )