Definition df-3or 921

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

This definition is referenced by:  3orass  923  3orrot  926  3ioran  935  3orbi123i  1129  3ori  1232  3jao  1233  mpjao3dan  1239  3orbi123d  1243  3orim123d  1252  3or6  1255  ecase23d  1282  hb3or  1482  eueq3dc  2767  eltpg  3440  rextpg  3448  nntri3or  6130  nntri1  6133  nnsseleq  6138  elznn0nn  8435  zleloe  8468  uzm1  8719  xrnemnf  8918  xrnepnf  8919  xrltso  8936  sizefiv01gt1  9795  bd3or  10763