Definition df-3or 980

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

This definition is referenced by:  3orass  982  3orrot  985  3ioran  994  3orbi123i  1190  3ori  1310  3jao  1311  mpjao3dan  1317  3orbi123d  1321  3orim123d  1330  3or6  1333  ecase23d  1360  hb3or  1559  eueq3dc  2923  eltpg  3649  rextpg  3658  nntri3or  6507  nntri1  6510  nnsseleq  6515  elznn0nn  9280  zleloe  9313  uzm1  9571  xrnemnf  9790  xrnepnf  9791  xrltso  9809  hashfiv01gt1  10775  prm23ge5  12277  bd3or  14808  triap  15005