Definition df-3or 964

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 757. (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 962	. 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒)
5	1, 2	wo 698	. . 3 wff (𝜑 ∨ 𝜓)
6	5, 3	wo 698	. 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒)
7	4, 6	wb 104	1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))

This definition is referenced by:  3orass  966  3orrot  969  3ioran  978  3orbi123i  1172  3ori  1282  3jao  1283  mpjao3dan  1289  3orbi123d  1293  3orim123d  1302  3or6  1305  ecase23d  1332  hb3or  1529  eueq3dc  2886  eltpg  3606  rextpg  3615  nntri3or  6443  nntri1  6446  nnsseleq  6451  elznn0nn  9187  zleloe  9220  uzm1  9475  xrnemnf  9691  xrnepnf  9692  xrltso  9710  hashfiv01gt1  10668  prm23ge5  12155  bd3or  13501  triap  13697