Definition df-3or 964

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

This definition is referenced by:  3orass  966  3orrot  969  3ioran  978  3orbi123i  1172  3ori  1279  3jao  1280  mpjao3dan  1286  3orbi123d  1290  3orim123d  1299  3or6  1302  ecase23d  1329  hb3or  1529  eueq3dc  2862  eltpg  3576  rextpg  3585  nntri3or  6397  nntri1  6400  nnsseleq  6405  elznn0nn  9092  zleloe  9125  uzm1  9380  xrnemnf  9594  xrnepnf  9595  xrltso  9612  hashfiv01gt1  10560  bd3or  13198  triap  13399