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  3106  eueq3  3670  sspsstri  4058  eltpg  4644  rextpg  4657  tppreqb  4762  somo  5572  ordtri1  6351  ordeleqon  7729  bropopvvv  8034  soxp  8073  soseq  8103  swoso  8672  fsetexb  8805  en3lplem2  9526  cflim2  10177  entric  10471  entri2  10472  psslinpr  10946  ssxr  11206  relin01  11665  elznn0nn  12506  nn01to3  12858  xrnemnf  13035  xrnepnf  13036  xrsupss  13228  xrinfmss  13229  fzone1  13704  swrdnd  14582  swrdnnn0nd  14584  swrdnd0  14585  cshwshashlem1  17027  tosso  18344  pmltpc  25411  dyaddisj  25557  nosepdmlem  27655  mulsproplem13  28128  mulsproplem14  28129  legso  28675  lnhl  28691  cgracol  28904  colinearalg  28987  1to3vfriswmgr  30359  3o1cs  32538  3o2cs  32539  3o3cs  32540  3unrab  32581  tlt3  33054  cycpmco2  33217  3orit  35912  wl-df2-3mintru2  37692  mblfinlem2  37861  ts3or1  38356  ts3or2  38357  ts3or3  38358  3orrabdioph  43092  oneptri  43566  frege114d  44066  df3or2  44076  andi3or  44332  uneqsn  44333  clsk1indlem3  44351  sbc3or  44840  en3lplem2VD  45151  3orbi123VD  45157  sbc3orgVD  45158  sbcoreleleqVD  45166  el1fzopredsuc  47638  even3prm2  48032  usgrexmpl2nb1  48345  usgrexmpl2nb4  48348  reorelicc  49023