Definition df-3or 582

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 218.

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 580	. 2 wff (φ ∨ ψ ∨ χ)
5	1, 2	wo 195	. . 3 wff (φ ∨ ψ)
6	5, 3	wo 195	. 2 wff ((φ ∨ ψ) ∨ χ)
7	4, 6	wb 127	1 wff ((φ ∨ ψ ∨ χ) ↔ ((φ ∨ ψ) ∨ χ))

This definition is referenced by:  3orass 584  3orrot 587  bi3or 607  3jao 632  bi3ord 635  im3ord 637  hb3or 706  eueq3 1430  sspsstri 1572  eltp 1834  wereu 2197  ordtri3or 2230  ordtri1 2231  ordtri3 2234  ordeleqon 2241  onzsl 2367  dflim3 2368  entri 3645  entri2 3646  psslinpr 3929  nnnegz 4566  elznn0nn 4575  elnnz1 4581  halfnz 4586

metamath.org