Definition df-3or 1087

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

This definition is referenced by:  3orass  1089  3orrot  1091  3ioran  1105  3ianor  1106  3orbi123i  1156  3ori  1426  3jao  1427  3jaob  1428  3orbi123d  1437  3orim123d  1446  3or6  1449  3orel3  1488  3pm3.2ni  1490  cadan  1609  nf3or  1905  3r19.43  3109  eueq3  3694  sspsstri  4080  eltpg  4662  rextpg  4675  tppreqb  4781  somo  5600  ordtri1  6385  ordeleqon  7774  bropopvvv  8087  soxp  8126  soseq  8156  swoso  8751  fsetexb  8876  en3lplem2  9625  cflim2  10275  entric  10569  entri2  10570  psslinpr  11043  ssxr  11302  relin01  11759  elznn0nn  12600  nn01to3  12955  xrnemnf  13131  xrnepnf  13132  xrsupss  13323  xrinfmss  13324  swrdnd  14670  swrdnnn0nd  14672  swrdnd0  14673  cshwshashlem1  17113  tosso  18427  pmltpc  25401  dyaddisj  25547  nosepdmlem  27645  mulsproplem13  28071  mulsproplem14  28072  legso  28524  lnhl  28540  cgracol  28753  colinearalg  28835  1to3vfriswmgr  30207  3o1cs  32388  3o2cs  32389  3o3cs  32390  3unrab  32430  fzone1  32723  tlt3  32896  cycpmco2  33090  3orit  35679  wl-df2-3mintru2  37449  mblfinlem2  37628  ts3or1  38123  ts3or2  38124  ts3or3  38125  3orrabdioph  42753  oneptri  43228  frege114d  43729  df3or2  43739  andi3or  43995  uneqsn  43996  clsk1indlem3  44014  sbc3or  44505  en3lplem2VD  44816  3orbi123VD  44822  sbc3orgVD  44823  sbcoreleleqVD  44831  el1fzopredsuc  47302  even3prm2  47681  usgrexmpl2nb1  47984  usgrexmpl2nb4  47987  reorelicc  48638