Definition df-3or 1031

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 544. (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 1029	. 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒)
5	1, 2	wo 381	. . 3 wff (𝜑 ∨ 𝜓)
6	5, 3	wo 381	. 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒)
7	4, 6	wb 194	1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))

This definition is referenced by:  3orass  1033  3orrot  1036  3anor  1046  3ioran  1048  3orbi123i  1244  3ori  1379  3jao  1380  mpjao3dan  1386  3orbi123d  1389  3orim123d  1398  3or6  1401  cadan  1538  nf3or  1822  nf3orOLD  2232  eueq3  3347  sspsstri  3670  eltpg  4173  rextpg  4183  tppreqb  4276  somo  4982  ordtri1  5658  ordtri3OLD  5662  ordeleqon  6857  bropopvvv  7119  soxp  7154  swoso  7639  en3lplem2  8372  cflim2  8945  entric  9235  entri2  9236  psslinpr  9709  ssxr  9958  relin01  10403  elznn0nn  11226  nn01to3  11615  xrnemnf  11790  xrnepnf  11791  xrsupss  11969  xrinfmss  11970  swrdnd  13232  cshwshashlem1  15588  tosso  16807  pmltpc  22970  dyaddisj  23114  legso  25239  lnhl  25255  cgracol  25464  colinearalg  25535  clwwlknprop  26093  2wlkonot3v  26195  2spthonot3v  26196  1to3vfriswmgra  26327  3o1cs  28486  3o2cs  28487  3o3cs  28488  tlt3  28789  3orel3  30641  3pm3.2ni  30642  3orit  30644  soseq  30788  nobnddown  30893  mblfinlem2  32400  ts3or1  32913  ts3or2  32914  ts3or3  32915  3orrabdioph  36148  frege114d  36852  df3or2  36862  andi3or  37123  uneqsn  37124  clsk1indlem3  37144  sbc3or  37542  sbc3orgOLD  37546  en3lplem2VD  37884  3orbi123VD  37890  sbc3orgVD  37891  el1fzopredsuc  39732  1to3vfriswmgr  41431