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  1155  3ori  1423  3jao  1424  3jaob  1425  3orbi123d  1434  3orim123d  1443  3or6  1446  3orel3  1484  3pm3.2ni  1486  cadan  1605  nf3or  1902  eueq3  3719  sspsstri  4114  eltpg  4690  rextpg  4703  tppreqb  4809  somo  5634  ordtri1  6418  ordeleqon  7800  bropopvvv  8113  soxp  8152  soseq  8182  swoso  8777  fsetexb  8902  en3lplem2  9650  cflim2  10300  entric  10594  entri2  10595  psslinpr  11068  ssxr  11327  relin01  11784  elznn0nn  12624  nn01to3  12980  xrnemnf  13156  xrnepnf  13157  xrsupss  13347  xrinfmss  13348  swrdnd  14688  swrdnnn0nd  14690  swrdnd0  14691  cshwshashlem1  17129  tosso  18476  pmltpc  25498  dyaddisj  25644  nosepdmlem  27742  mulsproplem13  28168  mulsproplem14  28169  legso  28621  lnhl  28637  cgracol  28850  colinearalg  28939  1to3vfriswmgr  30308  3o1cs  32489  3o2cs  32490  3o3cs  32491  3unrab  32530  fzone1  32807  tlt3  32944  cycpmco2  33135  3orit  35695  wl-df2-3mintru2  37467  mblfinlem2  37644  ts3or1  38139  ts3or2  38140  ts3or3  38141  3orrabdioph  42770  oneptri  43245  frege114d  43747  df3or2  43757  andi3or  44013  uneqsn  44014  clsk1indlem3  44032  sbc3or  44529  en3lplem2VD  44841  3orbi123VD  44847  sbc3orgVD  44848  sbcoreleleqVD  44856  el1fzopredsuc  47274  even3prm2  47643  usgrexmpl2nb1  47926  usgrexmpl2nb4  47929  reorelicc  48559