Definition df-3or 982

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

This definition is referenced by:  3orass  984  3orrot  987  3ioran  996  3orbi123i  1192  3ori  1313  3jao  1314  mpjao3dan  1320  3orbi123d  1324  3orim123d  1333  3or6  1336  ecase23d  1363  hb3or  1573  eueq3dc  2954  eltpg  3688  rextpg  3697  nntri3or  6602  nntri1  6605  nnsseleq  6610  elznn0nn  9421  zleloe  9454  uzm1  9714  xrnemnf  9934  xrnepnf  9935  xrltso  9953  hashfiv01gt1  10964  swrdnd  11150  prm23ge5  12702  bd3or  15964  triap  16170