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

Definition df-3or 940
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 512. (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 938 . 2  wff  ( ph  \/  ps  \/  ch )
51, 2wo 359 . . 3  wff  ( ph  \/  ps )
65, 3wo 359 . 2  wff  ( (
ph  \/  ps )  \/  ch )
74, 6wb 178 1  wff  ( (
ph  \/  ps  \/  ch )  <->  ( ( ph  \/  ps )  \/  ch ) )
Colors of variables: wff set class
This definition is referenced by:  3orass  942  3orrot  945  3anor  953  3ioran  955  3orbi123i  1146  3ori  1247  3jao  1248  3orbi123d  1256  3orim123d  1265  3or6  1268  cadan  1388  nf3or  1739  eueq3  2908  sspsstri  3239  eltpg  3636  rextpg  3645  somo  4306  ordtri1  4383  ordtri3  4386  ordeleqon  4538  soxp  6148  swoso  6645  en3lplem2  7371  cflim2  7843  entric  8133  entri2  8134  psslinpr  8609  ssxr  8846  nnnegz  9980  elznn0nn  9990  xrnemnf  10413  xrnepnf  10414  xrsupss  10579  xrinfmss  10580  tosso  14090  pmltpc  18758  dyaddisj  18899  3orel3  23421  3pm3.2ni  23422  3orit  23424  relin01  23446  soseq  23609  axfelem10  23710  colinearalg  23899  anddi2  24293  fixpc  24446  3orrabdioph  26216  sbc3org  27332  en3lplem2VD  27654  3orbi123VD  27660  sbc3orgVD  27661
  Copyright terms: Public domain W3C validator