Definition df-3or 969

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 967	. 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  971  3orrot  974  3ioran  983  3orbi123i  1179  3ori  1290  3jao  1291  mpjao3dan  1297  3orbi123d  1301  3orim123d  1310  3or6  1313  ecase23d  1340  hb3or  1537  eueq3dc  2900  eltpg  3621  rextpg  3630  nntri3or  6461  nntri1  6464  nnsseleq  6469  elznn0nn  9205  zleloe  9238  uzm1  9496  xrnemnf  9713  xrnepnf  9714  xrltso  9732  hashfiv01gt1  10695  prm23ge5  12196  bd3or  13711  triap  13908