Definition df-3or 931

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 725. (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 929	. 2 wff ( ph \/ ps \/ ch )
5	1, 2	wo 670	. . 3 wff ( ph \/ ps )
6	5, 3	wo 670	. 2 wff ( ( ph \/ ps ) \/ ch )
7	4, 6	wb 104	1 wff ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )

This definition is referenced by:  3orass  933  3orrot  936  3ioran  945  3orbi123i  1139  3ori  1246  3jao  1247  mpjao3dan  1253  3orbi123d  1257  3orim123d  1266  3or6  1269  ecase23d  1296  hb3or  1496  eueq3dc  2811  eltpg  3516  rextpg  3524  nntri3or  6319  nntri1  6322  nnsseleq  6327  elznn0nn  8920  zleloe  8953  uzm1  9206  xrnemnf  9405  xrnepnf  9406  xrltso  9423  hashfiv01gt1  10369  bd3or  12608  triap  12808