Definition df-3or 776

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	|- ((ph \/ ps \/ ch) <-> ((ph \/ ps) \/ ch))

Detailed syntax breakdown of Definition df-3or

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		wps	. . 3 wff ps
3		wch	. . 3 wff ch
4	1, 2, 3	w3o 774	. 2 wff (ph \/ ps \/ ch)
5	1, 2	wo 222	. . 3 wff (ph \/ ps)
6	5, 3	wo 222	. 2 wff ((ph \/ ps) \/ ch)
7	4, 6	wb 146	1 wff ((ph \/ ps \/ ch) <-> ((ph \/ ps) \/ ch))

This definition is referenced by:  3orass 778  3orrot 781  3orbi123i 823  3ori 885  3jao 886  3orbi123d 892  3orim123d 901  hb3or 1011  eueq3 1919  sspsstri 2148  eltp 2439  wereu 2945  ordtri3or 2979  ordtri1 2980  ordtri3 2983  ordeleqon 2990  onzsl 3117  dflim3 3118  entri 4839  entri2 4840  psslinpr 5135  lttri4t 5515  xrsupss 6078  xrinfmss 6079  nnnegz 6138  elznn0nn 6148  elnnz1 6155

Copyright terms: Public domain