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  1516  3pm3.2ni  1518  cadan  1641  nf3or  1937  3r19.43  3131  eueq3  3668  sspsstri  4033  eltpg  4646  rextpg  4659  tppreqb  4767  somo  5597  ordtri1  6396  ordeleqon  7796  bropopvvv  8101  soxp  8141  soseq  8176  swoso  8752  fsetexb  8886  en3lplem2  9614  cflim2  10341  entric  10641  entri2  10642  psslinpr  11116  ssxr  11379  relin01  11840  elznn0nn  12707  nn01to3  13068  xrnemnf  13246  xrnepnf  13247  xrsupss  13439  xrinfmss  13440  fzone1  13919  swrdnd  14804  swrdnnn0nd  14806  swrdnd0  14807  cshwshashlem1  17273  tosso  18591  pmltpc  25771  dyaddisj  25917  nosepdmlem  28040  mulsproplem13  28514  mulsproplem14  28515  legso  29062  lnhl  29081  plngrotlem2  29266  cgracol  29336  colinearalg  29488  1to3vfriswmgr  30881  3o1cs  33101  3o2cs  33102  3o3cs  33103  3unrab  33141  tlt3  33573  cycpmco2  33736  3orit  36523  wl-df2-3mintru2  38451  mblfinlem2  38619  ts3or1  39128  ts3or2  39129  ts3or3  39130  3orrabdioph  43836  oneptri  44301  frege114d  44800  df3or2  44810  andi3or  45066  uneqsn  45067  clsk1indlem3  45085  sbc3or  45557  en3lplem2VD  45868  3orbi123VD  45874  sbc3orgVD  45875  sbcoreleleqVD  45883  el1fzopredsuc  48438  even3prm2  48859  usgrexmpl2nb1  49172  usgrexmpl2nb4  49175  reorelicc  49864