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  7784  bropopvvv  8090  soxp  8130  soseq  8160  swoso  8734  fsetexb  8868  en3lplem2  9595  cflim2  10268  entric  10568  entri2  10569  psslinpr  11043  ssxr  11306  relin01  11765  elznn0nn  12632  nn01to3  12993  xrnemnf  13170  xrnepnf  13171  xrsupss  13363  xrinfmss  13364  fzone1  13842  swrdnd  14726  swrdnnn0nd  14728  swrdnd0  14729  cshwshashlem1  17191  tosso  18509  pmltpc  25679  dyaddisj  25825  nosepdmlem  27917  mulsproplem13  28391  mulsproplem14  28392  legso  28939  lnhl  28958  plngrotlem2  29143  cgracol  29213  colinearalg  29353  1to3vfriswmgr  30746  3o1cs  32924  3o2cs  32925  3o3cs  32926  3unrab  32964  tlt3  33397  cycpmco2  33560  3orit  36282  wl-df2-3mintru2  38226  mblfinlem2  38394  ts3or1  38888  ts3or2  38889  ts3or3  38890  3orrabdioph  43615  oneptri  44085  frege114d  44585  df3or2  44595  andi3or  44851  uneqsn  44852  clsk1indlem3  44870  sbc3or  45342  en3lplem2VD  45653  3orbi123VD  45659  sbc3orgVD  45660  sbcoreleleqVD  45668  el1fzopredsuc  48201  even3prm2  48622  usgrexmpl2nb1  48935  usgrexmpl2nb4  48938  reorelicc  49627