Definition df-3or 1104

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 935. (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 1102	. 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒)
5	1, 2	wo 861	. . 3 wff (𝜑 ∨ 𝜓)
6	5, 3	wo 861	. 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒)
7	4, 6	wb 209	1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))

This definition is used by:  3orass  1106  3orrot  1108  3ioran  1123  3ianor  1124  3orbi123i  1174  3ori  1452  3jao  1453  3jaob  1454  3orbi123d  1464  3orim123d  1473  3or6  1477  ecase33d  1505  3orel3  1517  3pm3.2ni  1519  cadan  1642  nf3or  1940  3r19.43  3135  eueq3  3672  sspsstri  4036  eltpg  4647  rextpg  4660  tppreqb  4768  somo  5602  ordtri1  6411  ordeleqon  7817  bropopvvv  8123  soxp  8165  soseq  8200  swoso  8777  fsetexb  8911  en3lplem2  9638  cflim2  10365  entric  10665  entri2  10666  psslinpr  11140  ssxr  11403  relin01  11864  elznn0nn  12731  nn01to3  13092  xrnemnf  13270  xrnepnf  13271  xrsupss  13463  xrinfmss  13464  fzone1  13943  swrdnd  14829  swrdnnn0nd  14831  swrdnd0  14832  cshwshashlem1  17299  tosso  18617  pmltpc  25798  dyaddisj  25944  nosepdmlem  28067  mulsproplem13  28541  mulsproplem14  28542  legso  29089  lnhl  29108  plngrotlem2  29293  cgracol  29363  colinearalg  29515  1to3vfriswmgr  30908  3o1cs  33128  3o2cs  33129  3o3cs  33130  3unrab  33168  tlt3  33598  cycpmco2  33761  3orit  36658  wl-df2-3mintru2  38599  mblfinlem2  38767  ts3or1  39276  ts3or2  39277  ts3or3  39278  3orrabdioph  43985  oneptri  44449  frege114d  44948  df3or2  44958  andi3or  45214  uneqsn  45215  clsk1indlem3  45233  sbc3or  45704  en3lplem2VD  46015  3orbi123VD  46021  sbc3orgVD  46022  sbcoreleleqVD  46030  el1fzopredsuc  48599  even3prm2  49020  usgrexmpl2nb1  49333  usgrexmpl2nb4  49336  reorelicc  50025