Definition df-3or 979

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

This definition is referenced by:  3orass  981  3orrot  984  3ioran  993  3orbi123i  1189  3ori  1300  3jao  1301  mpjao3dan  1307  3orbi123d  1311  3orim123d  1320  3or6  1323  ecase23d  1350  hb3or  1549  eueq3dc  2913  eltpg  3639  rextpg  3648  nntri3or  6496  nntri1  6499  nnsseleq  6504  elznn0nn  9269  zleloe  9302  uzm1  9560  xrnemnf  9779  xrnepnf  9780  xrltso  9798  hashfiv01gt1  10764  prm23ge5  12266  bd3or  14666  triap  14862