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  1427  3jao  1428  3jaob  1429  3orbi123d  1438  3orim123d  1447  3or6  1450  3orel3  1489  3pm3.2ni  1491  cadan  1611  nf3or  1907  3r19.43  3104  eueq3  3654  sspsstri  4038  eltpg  4620  rextpg  4633  tppreqb  4740  somo  5567  ordtri1  6345  ordeleqon  7725  bropopvvv  8029  soxp  8068  soseq  8098  swoso  8667  fsetexb  8800  en3lplem2  9523  cflim2  10174  entric  10468  entri2  10469  psslinpr  10943  ssxr  11204  relin01  11663  elznn0nn  12527  nn01to3  12880  xrnemnf  13057  xrnepnf  13058  xrsupss  13250  xrinfmss  13251  fzone1  13728  swrdnd  14606  swrdnnn0nd  14608  swrdnd0  14609  cshwshashlem1  17055  tosso  18372  pmltpc  25405  dyaddisj  25551  nosepdmlem  27635  mulsproplem13  28108  mulsproplem14  28109  legso  28655  lnhl  28671  cgracol  28884  colinearalg  28967  1to3vfriswmgr  30338  3o1cs  32518  3o2cs  32519  3o3cs  32520  3unrab  32561  tlt3  33018  cycpmco2  33182  3orit  35886  wl-df2-3mintru2  37789  mblfinlem2  37967  ts3or1  38462  ts3or2  38463  ts3or3  38464  3orrabdioph  43203  oneptri  43673  frege114d  44173  df3or2  44183  andi3or  44439  uneqsn  44440  clsk1indlem3  44458  sbc3or  44947  en3lplem2VD  45258  3orbi123VD  45264  sbc3orgVD  45265  sbcoreleleqVD  45273  el1fzopredsuc  47762  even3prm2  48183  usgrexmpl2nb1  48496  usgrexmpl2nb4  48499  reorelicc  49174