Definition df-3or 1090

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

This definition is referenced by:  3orass  1092  3orrot  1094  3ioran  1108  3ianor  1109  3orbi123i  1158  3ori  1426  3jao  1427  mpjao3danOLD  1434  3orbi123d  1437  3orim123d  1446  3or6  1449  cadan  1616  nf3or  1913  eueq3  3642  sspsstri  4034  eltpg  4618  rextpg  4632  tppreqb  4735  somo  5530  ordtri1  6281  ordeleqon  7606  bropopvvv  7898  soxp  7938  swoso  8466  fsetexb  8587  en3lplem2  9276  cflim2  9925  entric  10219  entri2  10220  psslinpr  10693  ssxr  10950  relin01  11404  elznn0nn  12238  nn01to3  12585  xrnemnf  12757  xrnepnf  12758  xrsupss  12947  xrinfmss  12948  swrdnd  14270  swrdnnn0nd  14272  swrdnd0  14273  cshwshashlem1  16700  tosso  18027  pmltpc  24494  dyaddisj  24640  legso  26839  lnhl  26855  cgracol  27068  colinearalg  27156  1to3vfriswmgr  28520  3o1cs  30688  3o2cs  30689  3o3cs  30690  fzone1  30998  tlt3  31125  cycpmco2  31277  3orel3  33532  3pm3.2ni  33533  3orit  33535  otthne  33560  soseq  33705  nosepdmlem  33788  wl-df2-3mintru2  35562  mblfinlem2  35721  ts3or1  36217  ts3or2  36218  ts3or3  36219  3orrabdioph  40493  frege114d  41228  df3or2  41238  andi3or  41494  uneqsn  41495  clsk1indlem3  41515  sbc3or  42014  en3lplem2VD  42326  3orbi123VD  42332  sbc3orgVD  42333  sbcoreleleqVD  42341  el1fzopredsuc  44678  even3prm2  45032  reorelicc  45917