Definition df-3or 1088

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

This definition is referenced by:  3orass  1090  3orrot  1092  3ioran  1106  3ianor  1107  3orbi123i  1157  3ori  1426  3jao  1427  3jaob  1428  3orbi123d  1437  3orim123d  1446  3or6  1449  3orel3  1488  3pm3.2ni  1490  cadan  1609  nf3or  1905  eueq3  3717  sspsstri  4105  eltpg  4686  rextpg  4699  tppreqb  4805  somo  5631  ordtri1  6417  ordeleqon  7802  bropopvvv  8115  soxp  8154  soseq  8184  swoso  8779  fsetexb  8904  en3lplem2  9653  cflim2  10303  entric  10597  entri2  10598  psslinpr  11071  ssxr  11330  relin01  11787  elznn0nn  12627  nn01to3  12983  xrnemnf  13159  xrnepnf  13160  xrsupss  13351  xrinfmss  13352  swrdnd  14692  swrdnnn0nd  14694  swrdnd0  14695  cshwshashlem1  17133  tosso  18464  pmltpc  25485  dyaddisj  25631  nosepdmlem  27728  mulsproplem13  28154  mulsproplem14  28155  legso  28607  lnhl  28623  cgracol  28836  colinearalg  28925  1to3vfriswmgr  30299  3o1cs  32480  3o2cs  32481  3o3cs  32482  3unrab  32522  fzone1  32802  tlt3  32960  cycpmco2  33153  3orit  35716  wl-df2-3mintru2  37486  mblfinlem2  37665  ts3or1  38160  ts3or2  38161  ts3or3  38162  3orrabdioph  42794  oneptri  43269  frege114d  43771  df3or2  43781  andi3or  44037  uneqsn  44038  clsk1indlem3  44056  sbc3or  44552  en3lplem2VD  44864  3orbi123VD  44870  sbc3orgVD  44871  sbcoreleleqVD  44879  el1fzopredsuc  47337  even3prm2  47706  usgrexmpl2nb1  47991  usgrexmpl2nb4  47994  reorelicc  48631