Definition df-3or 782

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

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 780	. 2 wff (ph \/ ps \/ ch)
5	1, 2	wo 220	. . 3 wff (ph \/ ps)
6	5, 3	wo 220	. 2 wff ((ph \/ ps) \/ ch)
7	4, 6	wb 144	1 wff ((ph \/ ps \/ ch) <-> ((ph \/ ps) \/ ch))

This definition is referenced by:  3orass 784  3orrot 787  3orbi123i 829  3ori 891  3jao 892  3orbi123d 898  3orim123d 907  hb3or 1047  eueq3 1965  sspsstri 2200  eltp 2500  wereu 2972  ordtri3or 3007  ordtri1 3008  ordtri3 3011  ordeleqon 3144  onzsl 3200  dflim3 3201  entric 4988  entri2 4989  psslinpr 5289  lttri4 5669  xrsupss 6246  xrinfmss 6247  nnnegz 6306  elznn0nn 6316  elnnz1 6323  anddi2 10718  3jaao 11388  3anor 11389

Copyright terms: Public domain