Definition df-3or 974

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 762. (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 972	. 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒)
5	1, 2	wo 703	. . 3 wff (𝜑 ∨ 𝜓)
6	5, 3	wo 703	. 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒)
7	4, 6	wb 104	1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))

This definition is referenced by:  3orass  976  3orrot  979  3ioran  988  3orbi123i  1184  3ori  1295  3jao  1296  mpjao3dan  1302  3orbi123d  1306  3orim123d  1315  3or6  1318  ecase23d  1345  hb3or  1542  eueq3dc  2904  eltpg  3628  rextpg  3637  nntri3or  6472  nntri1  6475  nnsseleq  6480  elznn0nn  9226  zleloe  9259  uzm1  9517  xrnemnf  9734  xrnepnf  9735  xrltso  9753  hashfiv01gt1  10716  prm23ge5  12218  bd3or  13864  triap  14061