Definition df-3or 1006

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 775. (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 1004	. 2 wff ( ph \/ ps \/ ch )
5	1, 2	wo 716	. . 3 wff ( ph \/ ps )
6	5, 3	wo 716	. 2 wff ( ( ph \/ ps ) \/ ch )
7	4, 6	wb 105	1 wff ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )

This definition is referenced by:  3orass  1008  3orrot  1011  3ioran  1020  3orbi123i  1216  3ori  1337  3jao  1338  mpjao3dan  1344  3orbi123d  1348  3orim123d  1357  3or6  1360  ecase23d  1387  hb3or  1598  eueq3dc  2994  eltpg  3739  rextpg  3748  nntri3or  6739  nntri1  6742  nnsseleq  6747  elznn0nn  9608  zleloe  9641  uzm1  9903  xrnemnf  10129  xrnepnf  10130  xrltso  10148  hashfiv01gt1  11170  swrdnd  11376  prm23ge5  12987  bd3or  16725  triap  16939