Definition df-3or 1037

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 1035	. 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  1039  3orrot  1042  3anor  1052  3ioran  1054  3orbi123i  1250  3ori  1385  3jao  1386  mpjao3dan  1392  3orbi123d  1395  3orim123d  1404  3or6  1407  cadan  1545  nf3or  1832  nf3orOLD  2244  eueq3  3368  sspsstri  3693  eltpg  4205  rextpg  4215  tppreqb  4312  somo  5039  ordtri1  5725  ordtri3OLD  5729  ordeleqon  6950  bropopvvv  7215  soxp  7250  swoso  7735  en3lplem2  8472  cflim2  9045  entric  9339  entri2  9340  psslinpr  9813  ssxr  10067  relin01  10512  elznn0nn  11351  nn01to3  11741  xrnemnf  11911  xrnepnf  11912  xrsupss  12098  xrinfmss  12099  swrdnd  13386  cshwshashlem1  15745  tosso  16976  pmltpc  23159  dyaddisj  23304  legso  25428  lnhl  25444  cgracol  25653  colinearalg  25724  1to3vfriswmgr  27042  3o1cs  29197  3o2cs  29198  3o3cs  29199  tlt3  29492  3orel3  31355  3pm3.2ni  31356  3orit  31358  soseq  31505  nobnddown  31617  nosepdmlem  31620  mblfinlem2  33118  ts3or1  33631  ts3or2  33632  ts3or3  33633  3orrabdioph  36866  frege114d  37570  df3or2  37580  andi3or  37841  uneqsn  37842  clsk1indlem3  37862  sbc3or  38259  sbc3orgOLD  38263  en3lplem2VD  38601  3orbi123VD  38607  sbc3orgVD  38608  el1fzopredsuc  40662