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

This definition is referenced by:  3orass  1090  3orrot  1092  3ioran  1106  3ianor  1107  3orbi123i  1156  3ori  1424  3jao  1425  3jaob  1426  3orbi123d  1435  3orim123d  1444  3or6  1447  3orel3  1485  3pm3.2ni  1487  cadan  1606  nf3or  1904  eueq3  3733  sspsstri  4128  eltpg  4709  rextpg  4724  tppreqb  4830  somo  5646  ordtri1  6428  ordeleqon  7817  bropopvvv  8131  soxp  8170  soseq  8200  swoso  8797  fsetexb  8922  en3lplem2  9682  cflim2  10332  entric  10626  entri2  10627  psslinpr  11100  ssxr  11359  relin01  11814  elznn0nn  12653  nn01to3  13006  xrnemnf  13180  xrnepnf  13181  xrsupss  13371  xrinfmss  13372  swrdnd  14702  swrdnnn0nd  14704  swrdnd0  14705  cshwshashlem1  17143  tosso  18489  pmltpc  25504  dyaddisj  25650  nosepdmlem  27746  mulsproplem13  28172  mulsproplem14  28173  legso  28625  lnhl  28641  cgracol  28854  colinearalg  28943  1to3vfriswmgr  30312  3o1cs  32490  3o2cs  32491  3o3cs  32492  3unrab  32531  fzone1  32805  tlt3  32943  cycpmco2  33126  3orit  35678  wl-df2-3mintru2  37451  mblfinlem2  37618  ts3or1  38113  ts3or2  38114  ts3or3  38115  3orrabdioph  42739  oneptri  43218  frege114d  43720  df3or2  43730  andi3or  43986  uneqsn  43987  clsk1indlem3  44005  sbc3or  44503  en3lplem2VD  44815  3orbi123VD  44821  sbc3orgVD  44822  sbcoreleleqVD  44830  el1fzopredsuc  47240  even3prm2  47593  usgrexmpl2nb1  47847  usgrexmpl2nb4  47850  reorelicc  48444