Definition df-3or 1055

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 545. (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 1053	. 2 wff (𝜑 ∨ 𝜓 ∨ 𝜒)
5	1, 2	wo 382	. . 3 wff (𝜑 ∨ 𝜓)
6	5, 3	wo 382	. 2 wff ((𝜑 ∨ 𝜓) ∨ 𝜒)
7	4, 6	wb 196	1 wff ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ ((𝜑 ∨ 𝜓) ∨ 𝜒))

This definition is referenced by:  3orass  1057  3orrot  1061  3anorOLD  1072  3ioran  1073  3ianor  1074  3orbi123i  1271  3ori  1428  3jao  1429  mpjao3dan  1435  3orbi123d  1438  3orim123d  1447  3or6  1450  cadan  1588  nf3or  1875  nf3orOLD  2281  eueq3  3414  sspsstri  3742  eltpg  4259  rextpg  4269  tppreqb  4368  somo  5098  ordtri1  5794  ordtri3OLD  5798  ordeleqon  7030  bropopvvv  7300  soxp  7335  swoso  7820  en3lplem2  8550  cflim2  9123  entric  9417  entri2  9418  psslinpr  9891  ssxr  10145  relin01  10590  elznn0nn  11429  nn01to3  11819  xrnemnf  11989  xrnepnf  11990  xrsupss  12177  xrinfmss  12178  swrdnd  13478  cshwshashlem1  15849  tosso  17083  pmltpc  23265  dyaddisj  23410  legso  25539  lnhl  25555  cgracol  25764  colinearalg  25835  1to3vfriswmgr  27260  3o1cs  29437  3o2cs  29438  3o3cs  29439  tlt3  29793  3orel3  31719  3pm3.2ni  31720  3orit  31722  soseq  31879  nosepdmlem  31958  mblfinlem2  33577  ts3or1  34090  ts3or2  34091  ts3or3  34092  3orrabdioph  37664  frege114d  38367  df3or2  38377  andi3or  38637  uneqsn  38638  clsk1indlem3  38658  sbc3or  39055  sbc3orgOLD  39059  en3lplem2VD  39393  3orbi123VD  39399  sbc3orgVD  39400  el1fzopredsuc  41660  even3prm2  41953