Definition df-3or 968

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

This definition is referenced by:  3orass  970  3orrot  973  3ioran  982  3orbi123i  1178  3ori  1289  3jao  1290  mpjao3dan  1296  3orbi123d  1300  3orim123d  1309  3or6  1312  ecase23d  1339  hb3or  1536  eueq3dc  2895  eltpg  3615  rextpg  3624  nntri3or  6452  nntri1  6455  nnsseleq  6460  elznn0nn  9196  zleloe  9229  uzm1  9487  xrnemnf  9704  xrnepnf  9705  xrltso  9723  hashfiv01gt1  10684  prm23ge5  12173  bd3or  13546  triap  13742