Definition df-3or 1104

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 935. (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 1102	. 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒)
5	1, 2	wo 861	. . 3 wff (𝜑 ∨ 𝜓)
6	5, 3	wo 861	. 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒)
7	4, 6	wb 209	1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))

This definition is used by:  3orass  1106  3orrot  1108  3ioran  1123  3ianor  1124  3orbi123i  1174  3ori  1451  3jao  1452  3jaob  1453  3orbi123d  1463  3orim123d  1472  3or6  1476  ecase33d  1504  3orel3  1517  3pm3.2ni  1519  cadan  1642  nf3or  1938  3r19.43  3133  eueq3  3672  sspsstri  4057  eltpg  4650  rextpg  4663  tppreqb  4771  somo  5606  ordtri1  6395  ordeleqon  7785  bropopvvv  8091  soxp  8131  soseq  8161  swoso  8735  fsetexb  8869  en3lplem2  9596  cflim2  10269  entric  10569  entri2  10570  psslinpr  11044  ssxr  11307  relin01  11766  elznn0nn  12633  nn01to3  12994  xrnemnf  13172  xrnepnf  13173  xrsupss  13365  xrinfmss  13366  fzone1  13844  swrdnd  14728  swrdnnn0nd  14730  swrdnd0  14731  cshwshashlem1  17193  tosso  18511  pmltpc  25684  dyaddisj  25830  nosepdmlem  27927  mulsproplem13  28401  mulsproplem14  28402  legso  28949  lnhl  28968  plngrotlem2  29153  cgracol  29223  colinearalg  29375  1to3vfriswmgr  30768  3o1cs  32946  3o2cs  32947  3o3cs  32948  3unrab  32986  tlt3  33418  cycpmco2  33581  3orit  36303  wl-df2-3mintru2  38247  mblfinlem2  38415  ts3or1  38909  ts3or2  38910  ts3or3  38911  3orrabdioph  43636  oneptri  44106  frege114d  44606  df3or2  44616  andi3or  44872  uneqsn  44873  clsk1indlem3  44891  sbc3or  45363  en3lplem2VD  45674  3orbi123VD  45680  sbc3orgVD  45681  sbcoreleleqVD  45689  el1fzopredsuc  48222  even3prm2  48643  usgrexmpl2nb1  48956  usgrexmpl2nb4  48959  reorelicc  49648