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

Definition df-3or 983
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 526. (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 981 . 2  wff  ( ph  \/  ps  \/  ch )
51, 2wo 369 . . 3  wff  ( ph  \/  ps )
65, 3wo 369 . 2  wff  ( (
ph  \/  ps )  \/  ch )
74, 6wb 187 1  wff  ( (
ph  \/  ps  \/  ch )  <->  ( ( ph  \/  ps )  \/  ch ) )
Colors of variables: wff setvar class
This definition is referenced by:  3orass  985  3orrot  988  3anor  998  3ioran  1000  3orbi123i  1195  3ori  1324  3jao  1325  mpjao3dan  1331  3orbi123d  1334  3orim123d  1343  3or6  1346  cadan  1505  nf3or  1996  eueq3  3188  sspsstri  3510  eltpg  3985  rextpg  3995  tppreqb  4084  somo  4751  ordtri1  5418  ordtri3  5421  ordeleqon  6573  bropopvvv  6831  soxp  6864  swoso  7349  en3lplem2  8073  cflim2  8644  entric  8933  entri2  8934  psslinpr  9407  ssxr  9654  relin01  10089  elznn0nn  10902  nn01to3  11208  xrnemnf  11370  xrnepnf  11371  xrsupss  11545  xrinfmss  11546  swrdnd  12734  cshwshashlem1  15009  tosso  16225  pmltpc  22343  dyaddisj  22496  legso  24586  lnhl  24602  cgracol  24811  colinearalg  24882  clwwlknprop  25442  2wlkonot3v  25545  2spthonot3v  25546  1to3vfriswmgra  25677  3o1cs  28045  3o2cs  28046  3o3cs  28047  tlt3  28377  3orel3  30296  3pm3.2ni  30297  3orit  30299  soseq  30443  nobnddown  30539  mblfinlem2  31885  ts3or1  32302  ts3or2  32303  ts3or3  32304  3orrabdioph  35538  frege114d  36263  df3or2  36273  sbc3or  36802  sbc3orgOLD  36806  en3lplem2VD  37156  3orbi123VD  37162  sbc3orgVD  37163  el1fzopredsuc  38535
  Copyright terms: Public domain W3C validator