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 920. (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 845	. . 3 wff (𝜑 ∨ 𝜓)
6	5, 3	wo 845	. 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒)
7	4, 6	wb 205	1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))

This definition is referenced by:  3orass  1090  3orrot  1092  3ioran  1106  3ianor  1107  3orbi123i  1156  3ori  1424  3jao  1425  mpjao3danOLD  1432  3orbi123d  1435  3orim123d  1444  3or6  1447  3orel3  1486  3pm3.2ni  1488  cadan  1610  nf3or  1908  eueq3  3672  sspsstri  4067  eltpg  4651  rextpg  4665  tppreqb  4770  somo  5587  ordtri1  6355  ordeleqon  7721  bropopvvv  8027  soxp  8066  soseq  8096  swoso  8688  fsetexb  8809  en3lplem2  9558  cflim2  10208  entric  10502  entri2  10503  psslinpr  10976  ssxr  11233  relin01  11688  elznn0nn  12522  nn01to3  12875  xrnemnf  13047  xrnepnf  13048  xrsupss  13238  xrinfmss  13239  swrdnd  14554  swrdnnn0nd  14556  swrdnd0  14557  cshwshashlem1  16979  tosso  18322  pmltpc  24851  dyaddisj  24997  nosepdmlem  27068  legso  27604  lnhl  27620  cgracol  27833  colinearalg  27922  1to3vfriswmgr  29287  3o1cs  31455  3o2cs  31456  3o3cs  31457  fzone1  31771  tlt3  31900  cycpmco2  32052  3orit  34374  wl-df2-3mintru2  36029  mblfinlem2  36189  ts3or1  36685  ts3or2  36686  ts3or3  36687  3orrabdioph  41164  oneptri  41649  frege114d  42152  df3or2  42162  andi3or  42418  uneqsn  42419  clsk1indlem3  42437  sbc3or  42936  en3lplem2VD  43248  3orbi123VD  43254  sbc3orgVD  43255  sbcoreleleqVD  43263  el1fzopredsuc  45677  even3prm2  46031  reorelicc  46916