Definition df-3or 1038

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

This definition is referenced by:  3orass  1040  3orrot  1044  3anor  1054  3ioran  1056  3orbi123i  1252  3ori  1388  3jao  1389  mpjao3dan  1395  3orbi123d  1398  3orim123d  1407  3or6  1410  cadan  1548  nf3or  1835  nf3orOLD  2245  eueq3  3381  sspsstri  3709  eltpg  4227  rextpg  4237  tppreqb  4336  somo  5069  ordtri1  5756  ordtri3OLD  5760  ordeleqon  6988  bropopvvv  7255  soxp  7290  swoso  7775  en3lplem2  8512  cflim2  9085  entric  9379  entri2  9380  psslinpr  9853  ssxr  10107  relin01  10552  elznn0nn  11391  nn01to3  11781  xrnemnf  11951  xrnepnf  11952  xrsupss  12139  xrinfmss  12140  swrdnd  13432  cshwshashlem1  15802  tosso  17036  pmltpc  23219  dyaddisj  23364  legso  25494  lnhl  25510  cgracol  25719  colinearalg  25790  1to3vfriswmgr  27144  3o1cs  29309  3o2cs  29310  3o3cs  29311  tlt3  29665  3orel3  31593  3pm3.2ni  31594  3orit  31596  soseq  31751  nosepdmlem  31833  mblfinlem2  33447  ts3or1  33960  ts3or2  33961  ts3or3  33962  3orrabdioph  37347  frege114d  38050  df3or2  38060  andi3or  38320  uneqsn  38321  clsk1indlem3  38341  sbc3or  38738  sbc3orgOLD  38742  en3lplem2VD  39079  3orbi123VD  39085  sbc3orgVD  39086  el1fzopredsuc  41335  even3prm2  41628