Definition df-3or 1010

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

This definition is referenced by:  3orass  1012  3orrot  1015  3ioran  1024  3orbi123i  1220  3ori  1341  3jao  1342  mpjao3dan  1348  3orbi123d  1352  3orim123d  1361  3or6  1364  ecase23d  1391  hb3or  1602  eueq3dc  3000  eltpg  3753  rextpg  3762  nntri3or  6759  nntri1  6762  nnsseleq  6767  elznn0nn  9640  zleloe  9673  uzm1  9935  xrnemnf  10161  xrnepnf  10162  xrltso  10180  hashfiv01gt1  11202  swrdnd  11412  prm23ge5  13024  bd3or  16772  triap  16986