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  6771  nntri1  6774  nnsseleq  6779  elznn0nn  9667  zleloe  9700  uzm1  9968  xrnemnf  10195  xrnepnf  10196  xrltso  10214  hashfiv01gt1  11242  swrdnd  11452  prm23ge5  13071  bd3or  17077  triap  17301