Definition df-3or 1005

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 774. (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 1003	. 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒)
5	1, 2	wo 715	. . 3 wff (𝜑 ∨ 𝜓)
6	5, 3	wo 715	. 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒)
7	4, 6	wb 105	1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))

This definition is referenced by:  3orass  1007  3orrot  1010  3ioran  1019  3orbi123i  1215  3ori  1336  3jao  1337  mpjao3dan  1343  3orbi123d  1347  3orim123d  1356  3or6  1359  ecase23d  1386  hb3or  1597  eueq3dc  2980  eltpg  3714  rextpg  3723  nntri3or  6661  nntri1  6664  nnsseleq  6669  elznn0nn  9493  zleloe  9526  uzm1  9787  xrnemnf  10012  xrnepnf  10013  xrltso  10031  hashfiv01gt1  11045  swrdnd  11244  prm23ge5  12855  bd3or  16475  triap  16684