Definition df-3or 886

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 684. (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 884	. 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒)
5	1, 2	wo 629	. . 3 wff (𝜑 ∨ 𝜓)
6	5, 3	wo 629	. 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒)
7	4, 6	wb 98	1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))

This definition is referenced by:  3orass  888  3orrot  891  3ioran  900  3orbi123i  1094  3ori  1195  3jao  1196  mpjao3dan  1202  3orbi123d  1206  3orim123d  1215  3or6  1218  ecase23d  1240  hb3or  1441  eueq3dc  2715  eltpg  3416  rextpg  3424  nntri3or  6072  nntri1  6074  nnsseleq  6079  elznn0nn  8259  zleloe  8292  uzm1  8503  xrnemnf  8699  xrnepnf  8700  xrltso  8717  bd3or  9949