Definition df-3or 974

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

This definition is referenced by:  3orass  976  3orrot  979  3ioran  988  3orbi123i  1184  3ori  1295  3jao  1296  mpjao3dan  1302  3orbi123d  1306  3orim123d  1315  3or6  1318  ecase23d  1345  hb3or  1542  eueq3dc  2904  eltpg  3626  rextpg  3635  nntri3or  6470  nntri1  6473  nnsseleq  6478  elznn0nn  9215  zleloe  9248  uzm1  9506  xrnemnf  9723  xrnepnf  9724  xrltso  9742  hashfiv01gt1  10705  prm23ge5  12207  bd3or  13826  triap  14023