MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-3or 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  3101  sspsstri  3441  eltpg  3843  rextpg  3852  tppreqb  3931  somo  4529  ordtri1  4606  ordtri3  4609  ordeleqon  4760  bropopvvv  6417  soxp  6450  swoso  6927  en3lplem2  7660  cflim2  8132  entric  8421  entri2  8422  psslinpr  8897  ssxr  9134  nnnegz  10274  elznn0nn  10284  xrnemnf  10707  xrnepnf  10708  xrsupss  10876  xrinfmss  10877  tosso  14453  pmltpc  19335  dyaddisj  19476  3o1cs  23941  3o2cs  23942  3o3cs  23943  3orel3  25154  3pm3.2ni  25155  3orit  25157  relin01  25182  soseq  25509  nobnddown  25610  colinearalg  25797  mblfinlem  26190  3orrabdioph  26779  swrdnd  28074  shwrdssizelem2  28167  2wlkonot3v  28216  2spthonot3v  28217  1to3vfriswmgra  28255  sbc3org  28471  en3lplem2VD  28810  3orbi123VD  28816  sbc3orgVD  28817
  Copyright terms: Public domain W3C validator