Definition df-3or 1073

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 547. (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 1071	. 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒)
5	1, 2	wo 382	. . 3 wff (𝜑 ∨ 𝜓)
6	5, 3	wo 382	. 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒)
7	4, 6	wb 196	1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))

This definition is referenced by:  3orass  1075  3orrot  1077  3anorOLD  1094  3ioran  1095  3ianor  1096  3orbi123i  1159  3ori  1529  3jao  1530  mpjao3dan  1536  3orbi123d  1539  3orim123d  1548  3or6  1551  cadan  1689  nf3or  1976  nf3orOLD  2382  eueq3  3514  sspsstri  3843  eltpg  4363  rextpg  4373  tppreqb  4473  somo  5213  ordtri1  5909  ordtri3OLD  5913  ordeleqon  7145  bropopvvv  7415  soxp  7450  swoso  7936  en3lplem2  8673  cflim2  9269  entric  9563  entri2  9564  psslinpr  10037  ssxr  10291  relin01  10736  elznn0nn  11575  nn01to3  11966  xrnemnf  12136  xrnepnf  12137  xrsupss  12324  xrinfmss  12325  swrdnd  13624  cshwshashlem1  15996  tosso  17229  pmltpc  23411  dyaddisj  23556  legso  25685  lnhl  25701  cgracol  25910  colinearalg  25981  1to3vfriswmgr  27426  3o1cs  29610  3o2cs  29611  3o3cs  29612  tlt3  29966  3orel3  31892  3pm3.2ni  31893  3orit  31895  soseq  32052  nosepdmlem  32131  mblfinlem2  33752  ts3or1  34265  ts3or2  34266  ts3or3  34267  3orrabdioph  37841  frege114d  38544  df3or2  38554  andi3or  38814  uneqsn  38815  clsk1indlem3  38835  sbc3or  39232  sbc3orgOLD  39236  en3lplem2VD  39570  3orbi123VD  39576  sbc3orgVD  39577  el1fzopredsuc  41837  even3prm2  42130