Definition df-3or 982

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

This definition is referenced by:  3orass  984  3orrot  987  3ioran  996  3orbi123i  1192  3ori  1313  3jao  1314  mpjao3dan  1320  3orbi123d  1324  3orim123d  1333  3or6  1336  ecase23d  1363  hb3or  1573  eueq3dc  2949  eltpg  3680  rextpg  3689  nntri3or  6589  nntri1  6592  nnsseleq  6597  elznn0nn  9399  zleloe  9432  uzm1  9692  xrnemnf  9912  xrnepnf  9913  xrltso  9931  hashfiv01gt1  10940  swrdnd  11126  prm23ge5  12637  bd3or  15879  triap  16083