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  3131  eueq3  3668  sspsstri  4053  eltpg  4646  rextpg  4659  tppreqb  4767  somo  5594  ordtri1  6385  ordeleqon  7779  bropopvvv  8084  soxp  8124  soseq  8154  swoso  8730  fsetexb  8864  en3lplem2  9592  cflim2  10312  entric  10612  entri2  10613  psslinpr  11087  ssxr  11350  relin01  11809  elznn0nn  12676  nn01to3  13037  xrnemnf  13215  xrnepnf  13216  xrsupss  13408  xrinfmss  13409  fzone1  13887  swrdnd  14771  swrdnnn0nd  14773  swrdnd0  14774  cshwshashlem1  17234  tosso  18552  pmltpc  25732  dyaddisj  25878  nosepdmlem  27973  mulsproplem13  28447  mulsproplem14  28448  legso  28995  lnhl  29014  plngrotlem2  29199  cgracol  29269  colinearalg  29421  1to3vfriswmgr  30814  3o1cs  32992  3o2cs  32993  3o3cs  32994  3unrab  33032  tlt3  33464  cycpmco2  33627  3orit  36402  wl-df2-3mintru2  38328  mblfinlem2  38496  ts3or1  39005  ts3or2  39006  ts3or3  39007  3orrabdioph  43732  oneptri  44202  frege114d  44702  df3or2  44712  andi3or  44968  uneqsn  44969  clsk1indlem3  44987  sbc3or  45459  en3lplem2VD  45770  3orbi123VD  45776  sbc3orgVD  45777  sbcoreleleqVD  45785  el1fzopredsuc  48318  even3prm2  48739  usgrexmpl2nb1  49052  usgrexmpl2nb4  49055  reorelicc  49744