Definition df-3or 1084

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

This definition is referenced by:  3orass  1086  3orrot  1088  3ioran  1102  3ianor  1103  3orbi123i  1152  3ori  1420  3jao  1421  mpjao3danOLD  1428  3orbi123d  1431  3orim123d  1440  3or6  1443  cadan  1610  nf3or  1906  eueq3  3702  sspsstri  4079  eltpg  4623  rextpg  4635  tppreqb  4738  somo  5510  ordtri1  6224  ordeleqon  7503  bropopvvv  7785  soxp  7823  swoso  8322  en3lplem2  9076  cflim2  9685  entric  9979  entri2  9980  psslinpr  10453  ssxr  10710  relin01  11164  elznn0nn  11996  nn01to3  12342  xrnemnf  12513  xrnepnf  12514  xrsupss  12703  xrinfmss  12704  swrdnd  14016  swrdnnn0nd  14018  swrdnd0  14019  cshwshashlem1  16429  tosso  17646  pmltpc  24051  dyaddisj  24197  legso  26385  lnhl  26401  cgracol  26614  colinearalg  26696  1to3vfriswmgr  28059  3o1cs  30227  3o2cs  30228  3o3cs  30229  fzone1  30523  tlt3  30652  cycpmco2  30775  3orel3  32942  3pm3.2ni  32943  3orit  32945  soseq  33096  nosepdmlem  33187  mblfinlem2  34945  ts3or1  35446  ts3or2  35447  ts3or3  35448  3orrabdioph  39429  frege114d  40152  df3or2  40162  andi3or  40421  uneqsn  40422  clsk1indlem3  40442  sbc3or  40915  en3lplem2VD  41227  3orbi123VD  41233  sbc3orgVD  41234  sbcoreleleqVD  41242  el1fzopredsuc  43574  even3prm2  43933  reorelicc  44746