Definition df-3or 1085

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

This definition is referenced by:  3orass  1087  3orrot  1089  3ioran  1103  3ianor  1104  3orbi123i  1153  3ori  1421  3jao  1422  mpjao3danOLD  1429  3orbi123d  1432  3orim123d  1441  3or6  1444  cadan  1611  nf3or  1906  eueq3  3650  sspsstri  4030  eltpg  4583  rextpg  4595  tppreqb  4698  somo  5474  ordtri1  6192  ordeleqon  7483  bropopvvv  7768  soxp  7806  swoso  8305  en3lplem2  9060  cflim2  9674  entric  9968  entri2  9969  psslinpr  10442  ssxr  10699  relin01  11153  elznn0nn  11983  nn01to3  12329  xrnemnf  12500  xrnepnf  12501  xrsupss  12690  xrinfmss  12691  swrdnd  14007  swrdnnn0nd  14009  swrdnd0  14010  cshwshashlem1  16421  tosso  17638  pmltpc  24054  dyaddisj  24200  legso  26393  lnhl  26409  cgracol  26622  colinearalg  26704  1to3vfriswmgr  28065  3o1cs  30233  3o2cs  30234  3o3cs  30235  fzone1  30549  tlt3  30678  cycpmco2  30825  3orel3  33055  3pm3.2ni  33056  3orit  33058  soseq  33209  nosepdmlem  33300  wl-df2-3mintru2  34902  mblfinlem2  35095  ts3or1  35591  ts3or2  35592  ts3or3  35593  3orrabdioph  39724  frege114d  40459  df3or2  40469  andi3or  40725  uneqsn  40726  clsk1indlem3  40746  sbc3or  41238  en3lplem2VD  41550  3orbi123VD  41556  sbc3orgVD  41557  sbcoreleleqVD  41565  el1fzopredsuc  43882  even3prm2  44237  reorelicc  45124