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 3 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  1773  eueq3  2940  sspsstri  3278  eltpg  3676  rextpg  3685  somo  4348  ordtri1  4425  ordtri3  4428  ordeleqon  4580  soxp  6228  swoso  6691  en3lplem2  7417  cflim2  7889  entric  8179  entri2  8180  psslinpr  8655  ssxr  8892  nnnegz  10027  elznn0nn  10037  xrnemnf  10460  xrnepnf  10461  xrsupss  10627  xrinfmss  10628  tosso  14142  pmltpc  18810  dyaddisj  18951  3o1cs  23097  3o2cs  23098  3o3cs  23099  3orel3  24063  3pm3.2ni  24064  3orit  24066  relin01  24089  soseq  24254  nobnddown  24355  colinearalg  24538  anddi2  24941  fixpc  25094  3orrabdioph  26863  nbusgra  28143  1to3vfriswmgra  28185  sbc3org  28295  en3lplem2VD  28620  3orbi123VD  28626  sbc3orgVD  28627
  Copyright terms: Public domain W3C validator