Definition df-3or 885

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 683. (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 883	. 2 wff (ph \/ ps \/ ch)
5	1, 2	wo 628	. . 3 wff (ph \/ ps)
6	5, 3	wo 628	. 2 wff ((ph \/ ps) \/ ch)
7	4, 6	wb 98	1 wff ((ph \/ ps \/ ch) <-> ((ph \/ ps) \/ ch))

This definition is referenced by:  3orass  887  3orrot  890  3ioran  899  3orbi123i  1093  3ori  1194  3jao  1195  mpjao3dan  1201  3orbi123d  1205  3orim123d  1214  3or6  1217  ecase23d  1239  hb3or  1438  eueq3dc  2709  eltpg  3407  rextpg  3415  nntri3or  6011  nntri1  6013  elznn0nn  8015  zleloe  8048  uzm1  8259  xrnemnf  8449  xrnepnf  8450  xrltso  8467  bd3or  9264