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  3101  sspsstri  3441  eltpg  3843  rextpg  3852  tppreqb  3931  somo  4529  ordtri1  4606  ordtri3  4609  ordeleqon  4761  bropopvvv  6418  soxp  6451  swoso  6928  en3lplem2  7661  cflim2  8133  entric  8422  entri2  8423  psslinpr  8898  ssxr  9135  nnnegz  10275  elznn0nn  10285  xrnemnf  10708  xrnepnf  10709  xrsupss  10877  xrinfmss  10878  tosso  14455  pmltpc  19337  dyaddisj  19478  3o1cs  23943  3o2cs  23944  3o3cs  23945  3orel3  25156  3pm3.2ni  25157  3orit  25159  relin01  25184  soseq  25514  nobnddown  25621  colinearalg  25814  mblfinlem  26207  3orrabdioph  26796  swrdnd  28118  cshwssizelem2  28208  2wlkonot3v  28259  2spthonot3v  28260  1to3vfriswmgra  28298  sbc3org  28517  en3lplem2VD  28857  3orbi123VD  28863  sbc3orgVD  28864
  Copyright terms: Public domain W3C validator