Definition df-3or 1088

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 922. (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 1086	. 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒)
5	1, 2	wo 848	. . 3 wff (𝜑 ∨ 𝜓)
6	5, 3	wo 848	. 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒)
7	4, 6	wb 206	1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))

This definition is referenced by:  3orass  1090  3orrot  1092  3ioran  1106  3ianor  1107  3orbi123i  1157  3ori  1427  3jao  1428  3jaob  1429  3orbi123d  1438  3orim123d  1447  3or6  1450  3orel3  1489  3pm3.2ni  1491  cadan  1611  nf3or  1907  3r19.43  3107  eueq3  3658  sspsstri  4046  eltpg  4631  rextpg  4644  tppreqb  4751  somo  5575  ordtri1  6354  ordeleqon  7733  bropopvvv  8037  soxp  8076  soseq  8106  swoso  8675  fsetexb  8808  en3lplem2  9531  cflim2  10182  entric  10476  entri2  10477  psslinpr  10951  ssxr  11212  relin01  11671  elznn0nn  12535  nn01to3  12888  xrnemnf  13065  xrnepnf  13066  xrsupss  13258  xrinfmss  13259  fzone1  13736  swrdnd  14614  swrdnnn0nd  14616  swrdnd0  14617  cshwshashlem1  17063  tosso  18380  pmltpc  25414  dyaddisj  25560  nosepdmlem  27644  mulsproplem13  28117  mulsproplem14  28118  legso  28664  lnhl  28680  cgracol  28893  colinearalg  28976  1to3vfriswmgr  30347  3o1cs  32527  3o2cs  32528  3o3cs  32529  3unrab  32570  tlt3  33027  cycpmco2  33191  3orit  35895  wl-df2-3mintru2  37798  mblfinlem2  37976  ts3or1  38471  ts3or2  38472  ts3or3  38473  3orrabdioph  43212  oneptri  43682  frege114d  44182  df3or2  44192  andi3or  44448  uneqsn  44449  clsk1indlem3  44467  sbc3or  44956  en3lplem2VD  45267  3orbi123VD  45273  sbc3orgVD  45274  sbcoreleleqVD  45282  el1fzopredsuc  47765  even3prm2  48186  usgrexmpl2nb1  48499  usgrexmpl2nb4  48502  reorelicc  49177