Definition df-3or 1103

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

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

This definition is referenced by:  3orass 1105  3orrot 1108  3anor 1113  3ioran 1115  3orbi123i 1307  3ori 1431  3jao 1432  3orbi123d 1440  3orim123d 1449  3or6 1452  hb3or 1647  eueq3 2675  sspsstri 2934  eltp 3267  wereu 3808  ordtri1 3844  ordtri3 3847  ordeleqon 4011  soxp 5213  en3lplem2 5993  sbc3org 6064  cflim2 6283  entric 6404  entri2 6405  psslinpr 6653  ssxr 6899  xrsupss 7627  xrinfmss 7628  nnnegz 7688  elznn0nn 7698  elnnz1 7705  3or6OLD 14435  3orel3 14438  3pm3.2ni 14439  3orit 14441  soxpOLD 14603  soseq 14608  axfelem10 14708  anddi2 14968  fixpc 15130  en3lplem2VD 17502  3orbi123VD 17508  sbc3orgVD 17509

Copyright terms: Public domain