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  9663  zleloe  9696  uzm1  9963  xrnemnf  10190  xrnepnf  10191  xrltso  10209  hashfiv01gt1  11237  swrdnd  11447  prm23ge5  13066  bd3or  17021  triap  17244