Definition df-3or 1087

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 919. (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 1085	. 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒)
5	1, 2	wo 844	. . 3 wff (𝜑 ∨ 𝜓)
6	5, 3	wo 844	. 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒)
7	4, 6	wb 205	1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))

This definition is referenced by:  3orass  1089  3orrot  1091  3ioran  1105  3ianor  1106  3orbi123i  1155  3ori  1423  3jao  1424  mpjao3danOLD  1431  3orbi123d  1434  3orim123d  1443  3or6  1446  3orel3  1485  3pm3.2ni  1487  cadan  1609  nf3or  1907  eueq3  3707  sspsstri  4102  eltpg  4689  rextpg  4703  tppreqb  4808  somo  5625  ordtri1  6397  ordeleqon  7773  bropopvvv  8081  soxp  8120  soseq  8150  swoso  8742  fsetexb  8864  en3lplem2  9614  cflim2  10264  entric  10558  entri2  10559  psslinpr  11032  ssxr  11290  relin01  11745  elznn0nn  12579  nn01to3  12932  xrnemnf  13104  xrnepnf  13105  xrsupss  13295  xrinfmss  13296  swrdnd  14611  swrdnnn0nd  14613  swrdnd0  14614  cshwshashlem1  17036  tosso  18382  pmltpc  25299  dyaddisj  25445  nosepdmlem  27530  mulsproplem13  27942  mulsproplem14  27943  legso  28284  lnhl  28300  cgracol  28513  colinearalg  28602  1to3vfriswmgr  29967  3o1cs  32137  3o2cs  32138  3o3cs  32139  fzone1  32445  tlt3  32574  cycpmco2  32729  3orit  35156  wl-df2-3mintru2  36832  mblfinlem2  36992  ts3or1  37487  ts3or2  37488  ts3or3  37489  3orrabdioph  41986  oneptri  42471  frege114d  42974  df3or2  42984  andi3or  43240  uneqsn  43241  clsk1indlem3  43259  sbc3or  43758  en3lplem2VD  44070  3orbi123VD  44076  sbc3orgVD  44077  sbcoreleleqVD  44085  el1fzopredsuc  46494  even3prm2  46848  reorelicc  47560