Definition df-3or 1089

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 1087	. 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒)
5	1, 2	wo 846	. . 3 wff (𝜑 ∨ 𝜓)
6	5, 3	wo 846	. 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒)
7	4, 6	wb 205	1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))

This definition is referenced by:  3orass  1091  3orrot  1093  3ioran  1107  3ianor  1108  3orbi123i  1157  3ori  1425  3jao  1426  mpjao3danOLD  1433  3orbi123d  1436  3orim123d  1445  3or6  1448  3orel3  1487  3pm3.2ni  1489  cadan  1611  nf3or  1909  eueq3  3708  sspsstri  4103  eltpg  4690  rextpg  4704  tppreqb  4809  somo  5626  ordtri1  6398  ordeleqon  7769  bropopvvv  8076  soxp  8115  soseq  8145  swoso  8736  fsetexb  8858  en3lplem2  9608  cflim2  10258  entric  10552  entri2  10553  psslinpr  11026  ssxr  11283  relin01  11738  elznn0nn  12572  nn01to3  12925  xrnemnf  13097  xrnepnf  13098  xrsupss  13288  xrinfmss  13289  swrdnd  14604  swrdnnn0nd  14606  swrdnd0  14607  cshwshashlem1  17029  tosso  18372  pmltpc  24967  dyaddisj  25113  nosepdmlem  27186  mulsproplem13  27584  mulsproplem14  27585  legso  27850  lnhl  27866  cgracol  28079  colinearalg  28168  1to3vfriswmgr  29533  3o1cs  31703  3o2cs  31704  3o3cs  31705  fzone1  32011  tlt3  32140  cycpmco2  32292  3orit  34685  wl-df2-3mintru2  36366  mblfinlem2  36526  ts3or1  37021  ts3or2  37022  ts3or3  37023  3orrabdioph  41521  oneptri  42006  frege114d  42509  df3or2  42519  andi3or  42775  uneqsn  42776  clsk1indlem3  42794  sbc3or  43293  en3lplem2VD  43605  3orbi123VD  43611  sbc3orgVD  43612  sbcoreleleqVD  43620  el1fzopredsuc  46033  even3prm2  46387  reorelicc  47396