Definition df-3or 1006

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 775. (Contributed by NM, 8-Apr-1994.)

Assertion

Ref	Expression
df-3or	⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))

Detailed syntax breakdown of Definition df-3or

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3		wch	. . 3 wff 𝜒
4	1, 2, 3	w3o 1004	. 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒)
5	1, 2	wo 716	. . 3 wff (𝜑 ∨ 𝜓)
6	5, 3	wo 716	. 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒)
7	4, 6	wb 105	1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))

This definition is referenced by:  3orass  1008  3orrot  1011  3ioran  1020  3orbi123i  1216  3ori  1337  3jao  1338  mpjao3dan  1344  3orbi123d  1348  3orim123d  1357  3or6  1360  ecase23d  1387  hb3or  1598  eueq3dc  2981  eltpg  3718  rextpg  3727  nntri3or  6704  nntri1  6707  nnsseleq  6712  elznn0nn  9554  zleloe  9587  uzm1  9848  xrnemnf  10073  xrnepnf  10074  xrltso  10092  hashfiv01gt1  11107  swrdnd  11306  prm23ge5  12917  bd3or  16545  triap  16761