Definition df-3or 981

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 768. (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 979	. 2 wff ( ph \/ ps \/ ch )
5	1, 2	wo 709	. . 3 wff ( ph \/ ps )
6	5, 3	wo 709	. 2 wff ( ( ph \/ ps ) \/ ch )
7	4, 6	wb 105	1 wff ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) )

This definition is referenced by:  3orass  983  3orrot  986  3ioran  995  3orbi123i  1191  3ori  1312  3jao  1313  mpjao3dan  1319  3orbi123d  1323  3orim123d  1332  3or6  1335  ecase23d  1362  hb3or  1571  eueq3dc  2946  eltpg  3677  rextpg  3686  nntri3or  6578  nntri1  6581  nnsseleq  6586  elznn0nn  9385  zleloe  9418  uzm1  9678  xrnemnf  9898  xrnepnf  9899  xrltso  9917  hashfiv01gt1  10925  prm23ge5  12558  bd3or  15727  triap  15930