Definition df-3or 775

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

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 773	. 2 wff (φ ⋁ ψ ⋁ χ)
5	1, 2	wo 222	. . 3 wff (φ ⋁ ψ)
6	5, 3	wo 222	. 2 wff ((φ ⋁ ψ) ⋁ χ)
7	4, 6	wb 146	1 wff ((φ ⋁ ψ ⋁ χ) ↔ ((φ ⋁ ψ) ⋁ χ))

This definition is referenced by:  3orass 777  3orrot 780  3orbi123i 822  3ori 883  3jao 884  3orbi123d 890  3orim123d 899  hb3or 1009  eueq3 1915  sspsstri 2144  eltp 2435  wereu 2944  ordtri3or 2978  ordtri3orOLD 2979  ordtri1 2980  ordtri3 2983  ordeleqon 2990  onzsl 3117  dflim3 3118  entri 4831  entri2 4832  psslinpr 5127  lttri4t 5507  xrsupss 6045  xrinfmss 6046  nnnegz 6105  elznn0nn 6115  elnnz1 6122

Copyright terms: Public domain