Definition df-3or 923

Description: Define disjunction ('or') of 3 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 717. (Contributed by NM, 8-Apr-1994.)

Assertion

Ref	Expression
df-3or	|- ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )

Detailed syntax breakdown of Definition df-3or

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		wps	. . 3 wff ps
3		wch	. . 3 wff ch
4	1, 2, 3	w3o 921	. 2 wff ( ph \/ ps \/ ch )
5	1, 2	wo 662	. . 3 wff ( ph \/ ps )
6	5, 3	wo 662	. 2 wff ( ( ph \/ ps ) \/ ch )
7	4, 6	wb 103	1 wff ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )

This definition is referenced by:  3orass  925  3orrot  928  3ioran  937  3orbi123i  1131  3ori  1234  3jao  1235  mpjao3dan  1241  3orbi123d  1245  3orim123d  1254  3or6  1257  ecase23d  1284  hb3or  1484  eueq3dc  2779  eltpg  3465  rextpg  3473  nntri3or  6189  nntri1  6192  nnsseleq  6197  elznn0nn  8674  zleloe  8707  uzm1  8958  xrnemnf  9157  xrnepnf  9158  xrltso  9175  hashfiv01gt1  10039  bd3or  11077