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  3707  sspsstri  4102  eltpg  4689  rextpg  4703  tppreqb  4808  somo  5625  ordtri1  6397  ordeleqon  7771  bropopvvv  8078  soxp  8117  soseq  8147  swoso  8738  fsetexb  8860  en3lplem2  9610  cflim2  10260  entric  10554  entri2  10555  psslinpr  11028  ssxr  11287  relin01  11742  elznn0nn  12576  nn01to3  12929  xrnemnf  13101  xrnepnf  13102  xrsupss  13292  xrinfmss  13293  swrdnd  14608  swrdnnn0nd  14610  swrdnd0  14611  cshwshashlem1  17033  tosso  18376  pmltpc  25191  dyaddisj  25337  nosepdmlem  27410  mulsproplem13  27811  mulsproplem14  27812  legso  28105  lnhl  28121  cgracol  28334  colinearalg  28423  1to3vfriswmgr  29788  3o1cs  31958  3o2cs  31959  3o3cs  31960  fzone1  32266  tlt3  32395  cycpmco2  32550  3orit  34977  wl-df2-3mintru2  36669  mblfinlem2  36829  ts3or1  37324  ts3or2  37325  ts3or3  37326  3orrabdioph  41823  oneptri  42308  frege114d  42811  df3or2  42821  andi3or  43077  uneqsn  43078  clsk1indlem3  43096  sbc3or  43595  en3lplem2VD  43907  3orbi123VD  43913  sbc3orgVD  43914  sbcoreleleqVD  43922  el1fzopredsuc  46332  even3prm2  46686  reorelicc  47484