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 919. (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 844	. . 3 wff (𝜑 ∨ 𝜓)
6	5, 3	wo 844	. 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒)
7	4, 6	wb 205	1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))

This definition is referenced by:  3orass  1089  3orrot  1091  3ioran  1105  3ianor  1106  3orbi123i  1155  3ori  1423  3jao  1424  mpjao3danOLD  1431  3orbi123d  1434  3orim123d  1443  3or6  1446  3orel3  1485  cadan  1611  nf3or  1908  eueq3  3646  sspsstri  4037  eltpg  4621  rextpg  4635  tppreqb  4738  somo  5540  ordtri1  6299  ordeleqon  7632  bropopvvv  7930  soxp  7970  swoso  8531  fsetexb  8652  en3lplem2  9371  cflim2  10019  entric  10313  entri2  10314  psslinpr  10787  ssxr  11044  relin01  11499  elznn0nn  12333  nn01to3  12681  xrnemnf  12853  xrnepnf  12854  xrsupss  13043  xrinfmss  13044  swrdnd  14367  swrdnnn0nd  14369  swrdnd0  14370  cshwshashlem1  16797  tosso  18137  pmltpc  24614  dyaddisj  24760  legso  26960  lnhl  26976  cgracol  27189  colinearalg  27278  1to3vfriswmgr  28644  3o1cs  30812  3o2cs  30813  3o3cs  30814  fzone1  31121  tlt3  31248  cycpmco2  31400  3pm3.2ni  33656  3orit  33658  otthne  33682  soseq  33803  nosepdmlem  33886  wl-df2-3mintru2  35656  mblfinlem2  35815  ts3or1  36311  ts3or2  36312  ts3or3  36313  3orrabdioph  40605  frege114d  41366  df3or2  41376  andi3or  41632  uneqsn  41633  clsk1indlem3  41653  sbc3or  42152  en3lplem2VD  42464  3orbi123VD  42470  sbc3orgVD  42471  sbcoreleleqVD  42479  el1fzopredsuc  44817  even3prm2  45171  reorelicc  46056