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

Definition df-3or 937
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 511. (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 935 . 2  wff  ( ph  \/  ps  \/  ch )
51, 2wo 358 . . 3  wff  ( ph  \/  ps )
65, 3wo 358 . 2  wff  ( (
ph  \/  ps )  \/  ch )
74, 6wb 177 1  wff  ( (
ph  \/  ps  \/  ch )  <->  ( ( ph  \/  ps )  \/  ch ) )
Colors of variables: wff set class
This definition is referenced by:  3orass  939  3orrot  942  3anor  950  3ioran  952  3orbi123i  1143  3ori  1244  3jao  1245  3orbi123d  1253  3orim123d  1262  3or6  1265  cadan  1401  nf3or  1859  eueq3  3109  sspsstri  3449  eltpg  3851  rextpg  3860  tppreqb  3939  somo  4537  ordtri1  4614  ordtri3  4617  ordeleqon  4769  bropopvvv  6426  soxp  6459  swoso  6936  en3lplem2  7671  cflim2  8143  entric  8432  entri2  8433  psslinpr  8908  ssxr  9145  nnnegz  10285  elznn0nn  10295  xrnemnf  10718  xrnepnf  10719  xrsupss  10887  xrinfmss  10888  tosso  14465  pmltpc  19347  dyaddisj  19488  3o1cs  23953  3o2cs  23954  3o3cs  23955  3orel3  25166  3pm3.2ni  25167  3orit  25169  relin01  25194  soseq  25529  nobnddown  25656  colinearalg  25849  mblfinlem2  26244  3orrabdioph  26842  swrdnd  28182  cshwssizelem2  28281  2wlkonot3v  28342  2spthonot3v  28343  1to3vfriswmgra  28397  sbc3org  28616  en3lplem2VD  28956  3orbi123VD  28962  sbc3orgVD  28963
  Copyright terms: Public domain W3C validator