Definition df-3or 773

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 771	. 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 775  3orrot 778  3orbi123i 820  3ori 881  3jao 882  3orbi123d 888  3orim123d 897  hb3or 987  eueq3 1891  sspsstri 2119  eltp 2410  wereu 2908  ordtri3or 2942  ordtri1 2943  ordtri3 2946  ordeleqon 2953  onzsl 3080  dflim3 3081  entri 4762  entri2 4763  psslinpr 5058  lttri4t 5438  xrsupss 5976  xrinfmss 5977  nnnegz 6036  elznn0nn 6046  elnnz1 6053

Copyright terms: Public domain