Definition df-3or 963

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

This definition is referenced by:  3orass  965  3orrot  968  3ioran  977  3orbi123i  1171  3ori  1278  3jao  1279  mpjao3dan  1285  3orbi123d  1289  3orim123d  1298  3or6  1301  ecase23d  1328  hb3or  1528  eueq3dc  2858  eltpg  3569  rextpg  3577  nntri3or  6389  nntri1  6392  nnsseleq  6397  elznn0nn  9068  zleloe  9101  uzm1  9356  xrnemnf  9564  xrnepnf  9565  xrltso  9582  hashfiv01gt1  10528  bd3or  13027  triap  13224