Definition df-3or 1087

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 921. (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 1085	. 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒)
5	1, 2	wo 847	. . 3 wff (𝜑 ∨ 𝜓)
6	5, 3	wo 847	. 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒)
7	4, 6	wb 206	1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))

This definition is referenced by:  3orass  1089  3orrot  1091  3ioran  1105  3ianor  1106  3orbi123i  1156  3ori  1426  3jao  1427  3jaob  1428  3orbi123d  1437  3orim123d  1446  3or6  1449  3orel3  1488  3pm3.2ni  1490  cadan  1609  nf3or  1905  3r19.43  3098  eueq3  3673  sspsstri  4058  eltpg  4640  rextpg  4653  tppreqb  4759  somo  5570  ordtri1  6344  ordeleqon  7722  bropopvvv  8030  soxp  8069  soseq  8099  swoso  8666  fsetexb  8798  en3lplem2  9528  cflim2  10176  entric  10470  entri2  10471  psslinpr  10944  ssxr  11203  relin01  11662  elznn0nn  12503  nn01to3  12860  xrnemnf  13037  xrnepnf  13038  xrsupss  13229  xrinfmss  13230  swrdnd  14579  swrdnnn0nd  14581  swrdnd0  14582  cshwshashlem1  17025  tosso  18341  pmltpc  25367  dyaddisj  25513  nosepdmlem  27611  mulsproplem13  28054  mulsproplem14  28055  legso  28562  lnhl  28578  cgracol  28791  colinearalg  28873  1to3vfriswmgr  30242  3o1cs  32423  3o2cs  32424  3o3cs  32425  3unrab  32465  fzone1  32756  tlt3  32925  cycpmco2  33088  3orit  35691  wl-df2-3mintru2  37461  mblfinlem2  37640  ts3or1  38135  ts3or2  38136  ts3or3  38137  3orrabdioph  42759  oneptri  43233  frege114d  43734  df3or2  43744  andi3or  44000  uneqsn  44001  clsk1indlem3  44019  sbc3or  44509  en3lplem2VD  44820  3orbi123VD  44826  sbc3orgVD  44827  sbcoreleleqVD  44835  el1fzopredsuc  47313  even3prm2  47707  usgrexmpl2nb1  48020  usgrexmpl2nb4  48023  reorelicc  48699