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  3102  eueq3  3682  sspsstri  4068  eltpg  4650  rextpg  4663  tppreqb  4769  somo  5585  ordtri1  6365  ordeleqon  7758  bropopvvv  8069  soxp  8108  soseq  8138  swoso  8705  fsetexb  8837  en3lplem2  9566  cflim2  10216  entric  10510  entri2  10511  psslinpr  10984  ssxr  11243  relin01  11702  elznn0nn  12543  nn01to3  12900  xrnemnf  13077  xrnepnf  13078  xrsupss  13269  xrinfmss  13270  swrdnd  14619  swrdnnn0nd  14621  swrdnd0  14622  cshwshashlem1  17066  tosso  18378  pmltpc  25351  dyaddisj  25497  nosepdmlem  27595  mulsproplem13  28031  mulsproplem14  28032  legso  28526  lnhl  28542  cgracol  28755  colinearalg  28837  1to3vfriswmgr  30209  3o1cs  32390  3o2cs  32391  3o3cs  32392  3unrab  32432  fzone1  32723  tlt3  32896  cycpmco2  33090  3orit  35703  wl-df2-3mintru2  37473  mblfinlem2  37652  ts3or1  38147  ts3or2  38148  ts3or3  38149  3orrabdioph  42771  oneptri  43246  frege114d  43747  df3or2  43757  andi3or  44013  uneqsn  44014  clsk1indlem3  44032  sbc3or  44522  en3lplem2VD  44833  3orbi123VD  44839  sbc3orgVD  44840  sbcoreleleqVD  44848  el1fzopredsuc  47326  even3prm2  47720  usgrexmpl2nb1  48023  usgrexmpl2nb4  48026  reorelicc  48699