Definition df-3or 1088

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

This definition is referenced by:  3orass  1090  3orrot  1092  3ioran  1106  3ianor  1107  3orbi123i  1157  3ori  1427  3jao  1428  3jaob  1429  3orbi123d  1438  3orim123d  1447  3or6  1450  3orel3  1489  3pm3.2ni  1491  cadan  1611  nf3or  1907  3r19.43  3107  eueq3  3671  sspsstri  4059  eltpg  4645  rextpg  4658  tppreqb  4763  somo  5581  ordtri1  6360  ordeleqon  7739  bropopvvv  8044  soxp  8083  soseq  8113  swoso  8682  fsetexb  8815  en3lplem2  9536  cflim2  10187  entric  10481  entri2  10482  psslinpr  10956  ssxr  11216  relin01  11675  elznn0nn  12516  nn01to3  12868  xrnemnf  13045  xrnepnf  13046  xrsupss  13238  xrinfmss  13239  fzone1  13714  swrdnd  14592  swrdnnn0nd  14594  swrdnd0  14595  cshwshashlem1  17037  tosso  18354  pmltpc  25424  dyaddisj  25570  nosepdmlem  27668  mulsproplem13  28141  mulsproplem14  28142  legso  28689  lnhl  28705  cgracol  28918  colinearalg  29001  1to3vfriswmgr  30373  3o1cs  32553  3o2cs  32554  3o3cs  32555  3unrab  32596  tlt3  33069  cycpmco2  33233  3orit  35938  wl-df2-3mintru2  37767  mblfinlem2  37938  ts3or1  38433  ts3or2  38434  ts3or3  38435  3orrabdioph  43169  oneptri  43643  frege114d  44143  df3or2  44153  andi3or  44409  uneqsn  44410  clsk1indlem3  44428  sbc3or  44917  en3lplem2VD  45228  3orbi123VD  45234  sbc3orgVD  45235  sbcoreleleqVD  45243  el1fzopredsuc  47714  even3prm2  48108  usgrexmpl2nb1  48421  usgrexmpl2nb4  48424  reorelicc  49099