Definition df-3or 859

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

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

This definition is referenced by:  3orass 861  3orrot 864  3anor 869  3orbi123i 1057  3ori 1157  3jao 1158  3jaaoOLD 1165  3orbi123d 1167  3orim123d 1176  hb3or 1358  eueq3 2430  sspsstri 2711  eltp 3074  wereu 3654  ordtri3orOLD 3692  ordtri1 3693  ordtri1OLD 3694  ordtri3 3697  ordtri3OLD 3698  ordeleqon 3866  onzslOLD 3929  dflim3OLD 3931  en3lplem2 5757  sbc3org 5827  entric 5990  entri2 5991  psslinpr 6287  lttri4OLD 6685  ssxr 6714  xrsupss 7287  xrinfmss 7288  nnnegz 7347  elznn0nn 7357  elnnz1 7364  3or6 13804  3orel3 13807  3ioran 13808  3pm3.2ni 13809  3orit 13811  soxp 13950  soseq 13955  axfelem9 14039  anddi2 14268  fixpc 14418  en3lplem2VD 16668  3orbi123VD 16674  sbc3orgVD 16675

Copyright terms: Public domain