Definition df-3or 1003

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

This definition is referenced by:  3orass  1005  3orrot  1008  3ioran  1017  3orbi123i  1213  3ori  1334  3jao  1335  mpjao3dan  1341  3orbi123d  1345  3orim123d  1354  3or6  1357  ecase23d  1384  hb3or  1595  eueq3dc  2978  eltpg  3712  rextpg  3721  nntri3or  6654  nntri1  6657  nnsseleq  6662  elznn0nn  9481  zleloe  9514  uzm1  9775  xrnemnf  10000  xrnepnf  10001  xrltso  10019  hashfiv01gt1  11032  swrdnd  11227  prm23ge5  12824  bd3or  16334  triap  16543