Definition df-3or 1102

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

This definition is referenced by:  3orass  1104  3orrot  1106  3ioran  1121  3ianor  1122  3orbi123i  1172  3ori  1449  3jao  1450  3jaob  1451  3orbi123d  1461  3orim123d  1470  3or6  1474  ecase33d  1502  3orel3  1515  3pm3.2ni  1517  cadan  1637  nf3or  1933  3r19.43  3132  eueq3  3673  sspsstri  4059  eltpg  4651  rextpg  4664  tppreqb  4772  somo  5608  ordtri1  6394  ordeleqon  7780  bropopvvv  8084  soxp  8124  soseq  8154  swoso  8728  fsetexb  8860  en3lplem2  9581  cflim2  10246  entric  10540  entri2  10541  psslinpr  11015  ssxr  11278  relin01  11737  elznn0nn  12604  nn01to3  12964  xrnemnf  13141  xrnepnf  13142  xrsupss  13334  xrinfmss  13335  fzone1  13812  swrdnd  14691  swrdnnn0nd  14693  swrdnd0  14694  cshwshashlem1  17154  tosso  18472  pmltpc  25588  dyaddisj  25734  nosepdmlem  27823  mulsproplem13  28297  mulsproplem14  28298  legso  28844  lnhl  28863  plngrotlem2  29044  cgracol  29112  colinearalg  29226  1to3vfriswmgr  30597  3o1cs  32775  3o2cs  32776  3o3cs  32777  3unrab  32815  tlt3  33256  cycpmco2  33419  3orit  36162  wl-df2-3mintru2  38075  mblfinlem2  38253  ts3or1  38748  ts3or2  38749  ts3or3  38750  3orrabdioph  43462  oneptri  43932  frege114d  44432  df3or2  44442  andi3or  44698  uneqsn  44699  clsk1indlem3  44717  sbc3or  45189  en3lplem2VD  45500  3orbi123VD  45506  sbc3orgVD  45507  sbcoreleleqVD  45515  el1fzopredsuc  48008  even3prm2  48429  usgrexmpl2nb1  48742  usgrexmpl2nb4  48745  reorelicc  49435