Definition df-3or 1103

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 934. (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 1101	. 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒)
5	1, 2	wo 860	. . 3 wff (𝜑 ∨ 𝜓)
6	5, 3	wo 860	. 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒)
7	4, 6	wb 209	1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))

This definition is used by:  3orass  1105  3orrot  1107  3ioran  1122  3ianor  1123  3orbi123i  1173  3ori  1450  3jao  1451  3jaob  1452  3orbi123d  1462  3orim123d  1471  3or6  1475  ecase33d  1503  3orel3  1516  3pm3.2ni  1518  cadan  1638  nf3or  1934  3r19.43  3133  eueq3  3673  sspsstri  4059  eltpg  4651  rextpg  4664  tppreqb  4772  somo  5607  ordtri1  6394  ordeleqon  7779  bropopvvv  8083  soxp  8123  soseq  8153  swoso  8727  fsetexb  8859  en3lplem2  9580  cflim2  10253  entric  10547  entri2  10548  psslinpr  11022  ssxr  11285  relin01  11744  elznn0nn  12611  nn01to3  12971  xrnemnf  13148  xrnepnf  13149  xrsupss  13341  xrinfmss  13342  fzone1  13820  swrdnd  14699  swrdnnn0nd  14701  swrdnd0  14702  cshwshashlem1  17161  tosso  18479  pmltpc  25620  dyaddisj  25766  nosepdmlem  27858  mulsproplem13  28332  mulsproplem14  28333  legso  28879  lnhl  28898  plngrotlem2  29081  cgracol  29150  colinearalg  29271  1to3vfriswmgr  30642  3o1cs  32820  3o2cs  32821  3o3cs  32822  3unrab  32860  tlt3  33299  cycpmco2  33462  3orit  36216  wl-df2-3mintru2  38159  mblfinlem2  38337  ts3or1  38830  ts3or2  38831  ts3or3  38832  3orrabdioph  43542  oneptri  44012  frege114d  44512  df3or2  44522  andi3or  44778  uneqsn  44779  clsk1indlem3  44797  sbc3or  45269  en3lplem2VD  45580  3orbi123VD  45586  sbc3orgVD  45587  sbcoreleleqVD  45595  el1fzopredsuc  48091  even3prm2  48512  usgrexmpl2nb1  48825  usgrexmpl2nb4  48828  reorelicc  49518