Definition df-3or 1069

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 905. (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 1067	. 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒)
5	1, 2	wo 833	. . 3 wff (𝜑 ∨ 𝜓)
6	5, 3	wo 833	. 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒)
7	4, 6	wb 198	1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))

This definition is referenced by:  3orass  1071  3orrot  1073  3ioran  1086  3ianor  1087  3orbi123i  1136  3ori  1404  3jao  1405  mpjao3dan  1411  3orbi123d  1414  3orim123d  1423  3or6  1426  cadan  1572  nf3or  1868  eueq3  3617  sspsstri  3971  eltpg  4498  rextpg  4510  tppreqb  4613  somo  5363  ordtri1  6064  ordeleqon  7321  bropopvvv  7595  soxp  7630  swoso  8124  en3lplem2  8872  cflim2  9485  entric  9779  entri2  9780  psslinpr  10253  ssxr  10512  relin01  10967  elznn0nn  11810  nn01to3  12158  xrnemnf  12332  xrnepnf  12333  xrsupss  12521  xrinfmss  12522  swrdnd  13825  swrdnnn0nd  13827  swrdnd0  13828  cshwshashlem1  16288  tosso  17507  pmltpc  23757  dyaddisj  23903  legso  26090  lnhl  26106  cgracol  26319  colinearalg  26402  1to3vfriswmgr  27817  3o1cs  30011  3o2cs  30012  3o3cs  30013  tlt3  30384  3orel3  32462  3pm3.2ni  32463  3orit  32465  soseq  32617  nosepdmlem  32708  mblfinlem2  34371  ts3or1  34875  ts3or2  34876  ts3or3  34877  3orrabdioph  38776  frege114d  39466  df3or2  39476  andi3or  39735  uneqsn  39736  clsk1indlem3  39756  sbc3or  40285  en3lplem2VD  40597  3orbi123VD  40603  sbc3orgVD  40604  sbcoreleleqVD  40612  el1fzopredsuc  42932  even3prm2  43253  reorelicc  44066