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  1610  nf3or  1906  3r19.43  3105  eueq3  3669  sspsstri  4057  eltpg  4643  rextpg  4656  tppreqb  4761  somo  5571  ordtri1  6350  ordeleqon  7727  bropopvvv  8032  soxp  8071  soseq  8101  swoso  8669  fsetexb  8801  en3lplem2  9522  cflim2  10173  entric  10467  entri2  10468  psslinpr  10942  ssxr  11202  relin01  11661  elznn0nn  12502  nn01to3  12854  xrnemnf  13031  xrnepnf  13032  xrsupss  13224  xrinfmss  13225  fzone1  13700  swrdnd  14578  swrdnnn0nd  14580  swrdnd0  14581  cshwshashlem1  17023  tosso  18340  pmltpc  25407  dyaddisj  25553  nosepdmlem  27651  mulsproplem13  28124  mulsproplem14  28125  legso  28671  lnhl  28687  cgracol  28900  colinearalg  28983  1to3vfriswmgr  30355  3o1cs  32535  3o2cs  32536  3o3cs  32537  3unrab  32578  tlt3  33052  cycpmco2  33215  3orit  35910  wl-df2-3mintru2  37690  mblfinlem2  37859  ts3or1  38354  ts3or2  38355  ts3or3  38356  3orrabdioph  43025  oneptri  43499  frege114d  43999  df3or2  44009  andi3or  44265  uneqsn  44266  clsk1indlem3  44284  sbc3or  44773  en3lplem2VD  45084  3orbi123VD  45090  sbc3orgVD  45091  sbcoreleleqVD  45099  el1fzopredsuc  47571  even3prm2  47965  usgrexmpl2nb1  48278  usgrexmpl2nb4  48281  reorelicc  48956