MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-3or Unicode version

Definition df-3or 935
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 510. (Contributed by NM, 8-Apr-1994.)
Assertion
Ref Expression
df-3or  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ( ph  \/  ps )  \/  ch ) )

Detailed syntax breakdown of Definition df-3or
StepHypRef Expression
1 wph . . 3  wff  ph
2 wps . . 3  wff  ps
3 wch . . 3  wff  ch
41, 2, 3w3o 933 . 2  wff  ( ph  \/  ps  \/  ch )
51, 2wo 357 . . 3  wff  ( ph  \/  ps )
65, 3wo 357 . 2  wff  ( (
ph  \/  ps )  \/  ch )
74, 6wb 176 1  wff  ( (
ph  \/  ps  \/  ch )  <->  ( ( ph  \/  ps )  \/  ch ) )
Colors of variables: wff set class
This definition is referenced by:  3orass  937  3orrot  940  3anor  948  3ioran  950  3orbi123i  1141  3ori  1242  3jao  1243  3orbi123d  1251  3orim123d  1260  3or6  1263  cadan  1382  nf3or  1785  eueq3  2953  sspsstri  3291  eltpg  3689  rextpg  3698  somo  4364  ordtri1  4441  ordtri3  4444  ordeleqon  4596  soxp  6244  swoso  6707  en3lplem2  7433  cflim2  7905  entric  8195  entri2  8196  psslinpr  8671  ssxr  8908  nnnegz  10043  elznn0nn  10053  xrnemnf  10476  xrnepnf  10477  xrsupss  10643  xrinfmss  10644  tosso  14158  pmltpc  18826  dyaddisj  18967  3o1cs  23113  3o2cs  23114  3o3cs  23115  3orel3  24078  3pm3.2ni  24079  3orit  24081  relin01  24104  soseq  24325  nobnddown  24426  colinearalg  24610  anddi2  25044  fixpc  25197  3orrabdioph  26966  nbusgra  28277  trlonprop  28341  1to3vfriswmgra  28431  sbc3org  28594  en3lplem2VD  28936  3orbi123VD  28942  sbc3orgVD  28943
  Copyright terms: Public domain W3C validator