Definition df-3or 1094

Description: Define disjunction ('or') of three 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 928. (Contributed by NM, 8-Apr-1994.)

Assertion

Ref	Expression
df-3or	⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))

Detailed syntax breakdown of Definition df-3or

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		wps	. . 3 wff 𝜓
3		wch	. . 3 wff 𝜒
4	1, 2, 3	w3o 1092	. 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒)
5	1, 2	wo 854	. . 3 wff (𝜑 ∨ 𝜓)
6	5, 3	wo 854	. 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒)
7	4, 6	wb 208	1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))

This definition is referenced by:  3orass  1096  3orrot  1098  3ioran  1112  3ianor  1113  3orbi123i  1163  3ori  1433  3jao  1434  3jaob  1435  3orbi123d  1444  3orim123d  1453  3or6  1456  3orel3  1495  3pm3.2ni  1497  cadan  1617  nf3or  1913  3r19.43  3110  eueq3  3653  sspsstri  4038  eltpg  4620  rextpg  4633  tppreqb  4740  somo  5567  ordtri1  6346  ordeleqon  7728  bropopvvv  8031  soxp  8071  soseq  8101  swoso  8672  fsetexb  8805  en3lplem2  9529  cflim2  10181  entric  10475  entri2  10476  psslinpr  10950  ssxr  11211  relin01  11670  elznn0nn  12533  nn01to3  12886  xrnemnf  13063  xrnepnf  13064  xrsupss  13256  xrinfmss  13257  fzone1  13734  swrdnd  14612  swrdnnn0nd  14614  swrdnd0  14615  cshwshashlem1  17061  tosso  18378  pmltpc  25438  dyaddisj  25584  nosepdmlem  27667  mulsproplem13  28140  mulsproplem14  28141  legso  28687  lnhl  28703  cgracol  28916  colinearalg  28999  1to3vfriswmgr  30370  3o1cs  32550  3o2cs  32551  3o3cs  32552  3unrab  32593  tlt3  33051  cycpmco2  33216  3orit  35957  wl-df2-3mintru2  37860  mblfinlem2  38038  ts3or1  38533  ts3or2  38534  ts3or3  38535  3orrabdioph  43245  oneptri  43715  frege114d  44215  df3or2  44225  andi3or  44481  uneqsn  44482  clsk1indlem3  44500  sbc3or  44989  en3lplem2VD  45300  3orbi123VD  45306  sbc3orgVD  45307  sbcoreleleqVD  45315  el1fzopredsuc  47801  even3prm2  48222  usgrexmpl2nb1  48535  usgrexmpl2nb4  48538  reorelicc  49213