Definition df-3or 979

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

This definition is referenced by:  3orass  981  3orrot  984  3ioran  993  3orbi123i  1189  3ori  1300  3jao  1301  mpjao3dan  1307  3orbi123d  1311  3orim123d  1320  3or6  1323  ecase23d  1350  hb3or  1549  eueq3dc  2912  eltpg  3638  rextpg  3647  nntri3or  6494  nntri1  6497  nnsseleq  6502  elznn0nn  9267  zleloe  9300  uzm1  9558  xrnemnf  9777  xrnepnf  9778  xrltso  9796  hashfiv01gt1  10762  prm23ge5  12264  bd3or  14584  triap  14780