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  2993  eltpg  3736  rextpg  3745  nntri3or  6728  nntri1  6731  nnsseleq  6736  elznn0nn  9593  zleloe  9626  uzm1  9888  xrnemnf  10113  xrnepnf  10114  xrltso  10132  hashfiv01gt1  11149  swrdnd  11355  prm23ge5  12966  bd3or  16616  triap  16830