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  1572  eueq3dc  2947  eltpg  3678  rextpg  3687  nntri3or  6579  nntri1  6582  nnsseleq  6587  elznn0nn  9386  zleloe  9419  uzm1  9679  xrnemnf  9899  xrnepnf  9900  xrltso  9918  hashfiv01gt1  10927  swrdnd  11112  prm23ge5  12587  bd3or  15765  triap  15968