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

Definition df-3or 992
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 531. (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 990 . 2  wff  ( ph  \/  ps  \/  ch )
51, 2wo 374 . . 3  wff  ( ph  \/  ps )
65, 3wo 374 . 2  wff  ( (
ph  \/  ps )  \/  ch )
74, 6wb 189 1  wff  ( (
ph  \/  ps  \/  ch )  <->  ( ( ph  \/  ps )  \/  ch ) )
Colors of variables: wff setvar class
This definition is referenced by:  3orass  994  3orrot  997  3anor  1007  3ioran  1009  3orbi123i  1204  3ori  1337  3jao  1338  mpjao3dan  1344  3orbi123d  1347  3orim123d  1356  3or6  1359  cadan  1523  nf3or  2030  eueq3  3225  sspsstri  3547  eltpg  4026  rextpg  4036  tppreqb  4126  somo  4808  ordtri1  5475  ordtri3  5478  ordeleqon  6642  bropopvvv  6901  soxp  6936  swoso  7420  en3lplem2  8146  cflim2  8719  entric  9008  entri2  9009  psslinpr  9482  ssxr  9729  relin01  10166  elznn0nn  10980  nn01to3  11286  xrnemnf  11448  xrnepnf  11449  xrsupss  11623  xrinfmss  11624  swrdnd  12825  cshwshashlem1  15115  tosso  16331  pmltpc  22450  dyaddisj  22603  legso  24693  lnhl  24709  cgracol  24918  colinearalg  24989  clwwlknprop  25549  2wlkonot3v  25652  2spthonot3v  25653  1to3vfriswmgra  25784  3o1cs  28152  3o2cs  28153  3o3cs  28154  tlt3  28475  3orel3  30393  3pm3.2ni  30394  3orit  30396  soseq  30541  nobnddown  30639  mblfinlem2  32023  ts3or1  32440  ts3or2  32441  ts3or3  32442  3orrabdioph  35671  frege114d  36395  df3or2  36405  sbc3or  36933  sbc3orgOLD  36937  en3lplem2VD  37280  3orbi123VD  37286  sbc3orgVD  37287  el1fzopredsuc  38760
  Copyright terms: Public domain W3C validator