Definition df-3or 1100

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 932. (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 1098	. 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒)
5	1, 2	wo 858	. . 3 wff (𝜑 ∨ 𝜓)
6	5, 3	wo 858	. 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒)
7	4, 6	wb 208	1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))

This definition is referenced by:  3orass  1102  3orrot  1104  3ioran  1119  3ianor  1120  3orbi123i  1170  3ori  1445  3jao  1446  3jaob  1447  3orbi123d  1458  3orim123d  1467  3or6  1470  3orel3  1509  3pm3.2ni  1511  cadan  1631  nf3or  1927  3r19.43  3133  eueq3  3676  sspsstri  4061  eltpg  4647  rextpg  4660  tppreqb  4767  somo  5596  ordtri1  6381  ordeleqon  7767  bropopvvv  8071  soxp  8111  soseq  8141  swoso  8715  fsetexb  8847  en3lplem2  9570  cflim2  10222  entric  10516  entri2  10517  psslinpr  10991  ssxr  11254  relin01  11713  elznn0nn  12584  nn01to3  12944  xrnemnf  13121  xrnepnf  13122  xrsupss  13314  xrinfmss  13315  fzone1  13792  swrdnd  14670  swrdnnn0nd  14672  swrdnd0  14673  cshwshashlem1  17133  tosso  18451  pmltpc  25514  dyaddisj  25660  nosepdmlem  27749  mulsproplem13  28223  mulsproplem14  28224  legso  28770  lnhl  28786  plngrotlem2  28997  cgracol  29024  colinearalg  29113  1to3vfriswmgr  30484  3o1cs  32663  3o2cs  32664  3o3cs  32665  3unrab  32704  tlt3  33150  cycpmco2  33315  3orit  36071  wl-df2-3mintru2  37984  mblfinlem2  38162  ts3or1  38657  ts3or2  38658  ts3or3  38659  3orrabdioph  43369  oneptri  43839  frege114d  44339  df3or2  44349  andi3or  44605  uneqsn  44606  clsk1indlem3  44624  sbc3or  45113  en3lplem2VD  45424  3orbi123VD  45430  sbc3orgVD  45431  sbcoreleleqVD  45439  el1fzopredsuc  47925  even3prm2  48346  usgrexmpl2nb1  48659  usgrexmpl2nb4  48662  reorelicc  49337