Definition df-3or 1087

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

This definition is referenced by:  3orass  1089  3orrot  1091  3ioran  1105  3ianor  1106  3orbi123i  1156  3ori  1426  3jao  1427  3jaob  1428  3orbi123d  1437  3orim123d  1446  3or6  1449  3orel3  1488  3pm3.2ni  1490  cadan  1610  nf3or  1906  3r19.43  3101  eueq3  3665  sspsstri  4052  eltpg  4636  rextpg  4649  tppreqb  4754  somo  5561  ordtri1  6339  ordeleqon  7715  bropopvvv  8020  soxp  8059  soseq  8089  swoso  8656  fsetexb  8788  en3lplem2  9503  cflim2  10154  entric  10448  entri2  10449  psslinpr  10922  ssxr  11182  relin01  11641  elznn0nn  12482  nn01to3  12839  xrnemnf  13016  xrnepnf  13017  xrsupss  13208  xrinfmss  13209  fzone1  13684  swrdnd  14562  swrdnnn0nd  14564  swrdnd0  14565  cshwshashlem1  17007  tosso  18323  pmltpc  25378  dyaddisj  25524  nosepdmlem  27622  mulsproplem13  28067  mulsproplem14  28068  legso  28577  lnhl  28593  cgracol  28806  colinearalg  28888  1to3vfriswmgr  30260  3o1cs  32440  3o2cs  32441  3o3cs  32442  3unrab  32483  tlt3  32951  cycpmco2  33102  3orit  35760  wl-df2-3mintru2  37529  mblfinlem2  37708  ts3or1  38203  ts3or2  38204  ts3or3  38205  3orrabdioph  42886  oneptri  43360  frege114d  43861  df3or2  43871  andi3or  44127  uneqsn  44128  clsk1indlem3  44146  sbc3or  44635  en3lplem2VD  44946  3orbi123VD  44952  sbc3orgVD  44953  sbcoreleleqVD  44961  el1fzopredsuc  47435  even3prm2  47829  usgrexmpl2nb1  48142  usgrexmpl2nb4  48145  reorelicc  48821