Definition df-3or 920

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 716. (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 918	. 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒)
5	1, 2	wo 661	. . 3 wff (𝜑 ∨ 𝜓)
6	5, 3	wo 661	. 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒)
7	4, 6	wb 103	1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))

This definition is referenced by:  3orass  922  3orrot  925  3ioran  934  3orbi123i  1128  3ori  1231  3jao  1232  mpjao3dan  1238  3orbi123d  1242  3orim123d  1251  3or6  1254  ecase23d  1281  hb3or  1481  eueq3dc  2766  eltpg  3438  rextpg  3446  nntri3or  6095  nntri1  6097  nnsseleq  6102  elznn0nn  8365  zleloe  8398  uzm1  8649  xrnemnf  8853  xrnepnf  8854  xrltso  8871  bd3or  10620