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  3103  eueq3  3667  sspsstri  4055  eltpg  4641  rextpg  4654  tppreqb  4759  somo  5569  ordtri1  6348  ordeleqon  7725  bropopvvv  8030  soxp  8069  soseq  8099  swoso  8667  fsetexb  8799  en3lplem2  9520  cflim2  10171  entric  10465  entri2  10466  psslinpr  10940  ssxr  11200  relin01  11659  elznn0nn  12500  nn01to3  12852  xrnemnf  13029  xrnepnf  13030  xrsupss  13222  xrinfmss  13223  fzone1  13698  swrdnd  14576  swrdnnn0nd  14578  swrdnd0  14579  cshwshashlem1  17021  tosso  18338  pmltpc  25405  dyaddisj  25551  nosepdmlem  27649  mulsproplem13  28097  mulsproplem14  28098  legso  28620  lnhl  28636  cgracol  28849  colinearalg  28932  1to3vfriswmgr  30304  3o1cs  32484  3o2cs  32485  3o3cs  32486  3unrab  32527  tlt3  33001  cycpmco2  33164  3orit  35859  wl-df2-3mintru2  37629  mblfinlem2  37798  ts3or1  38293  ts3or2  38294  ts3or3  38295  3orrabdioph  42967  oneptri  43441  frege114d  43941  df3or2  43951  andi3or  44207  uneqsn  44208  clsk1indlem3  44226  sbc3or  44715  en3lplem2VD  45026  3orbi123VD  45032  sbc3orgVD  45033  sbcoreleleqVD  45041  el1fzopredsuc  47513  even3prm2  47907  usgrexmpl2nb1  48220  usgrexmpl2nb4  48223  reorelicc  48898