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 used 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  3754  rextpg  3763  nntri3or  6766  nntri1  6769  nnsseleq  6774  elznn0nn  9662  zleloe  9695  uzm1  9962  xrnemnf  10189  xrnepnf  10190  xrltso  10208  hashfiv01gt1  11235  swrdnd  11445  prm23ge5  13063  bd3or  16953  triap  17176