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  9658  zleloe  9691  uzm1  9953  xrnemnf  10179  xrnepnf  10180  xrltso  10198  hashfiv01gt1  11221  swrdnd  11431  prm23ge5  13043  bd3or  16855  triap  17078