Definition df-3or 981

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 768. (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 979	. 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒)
5	1, 2	wo 709	. . 3 wff (𝜑 ∨ 𝜓)
6	5, 3	wo 709	. 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒)
7	4, 6	wb 105	1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))

This definition is referenced by:  3orass  983  3orrot  986  3ioran  995  3orbi123i  1191  3ori  1311  3jao  1312  mpjao3dan  1318  3orbi123d  1322  3orim123d  1331  3or6  1334  ecase23d  1361  hb3or  1563  eueq3dc  2938  eltpg  3668  rextpg  3677  nntri3or  6560  nntri1  6563  nnsseleq  6568  elznn0nn  9357  zleloe  9390  uzm1  9649  xrnemnf  9869  xrnepnf  9870  xrltso  9888  hashfiv01gt1  10891  prm23ge5  12458  bd3or  15559  triap  15760