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  1507  nf3or  1994  eueq3  3252  sspsstri  3573  eltpg  4045  rextpg  4055  tppreqb  4144  somo  4809  ordtri1  5475  ordtri3  5478  ordeleqon  6629  bropopvvv  6887  soxp  6920  swoso  7402  en3lplem2  8120  cflim2  8691  entric  8980  entri2  8981  psslinpr  9455  ssxr  9702  relin01  10137  elznn0nn  10951  nn01to3  11257  xrnemnf  11419  xrnepnf  11420  xrsupss  11594  xrinfmss  11595  swrdnd  12773  cshwshashlem1  15029  tosso  16233  pmltpc  22282  dyaddisj  22431  legso  24504  cgracol  24724  colinearalg  24786  clwwlknprop  25345  2wlkonot3v  25448  2spthonot3v  25449  1to3vfriswmgra  25580  3o1cs  27938  3o2cs  27939  3o3cs  27940  tlt3  28264  3orel3  30132  3pm3.2ni  30133  3orit  30135  soseq  30279  nobnddown  30375  mblfinlem2  31682  ts3or1  32099  ts3or2  32100  ts3or3  32101  3orrabdioph  35335  frege114d  35989  sbc3or  36526  sbc3orgOLD  36530  en3lplem2VD  36880  3orbi123VD  36886  sbc3orgVD  36887  el1fzopredsuc  38112
  Copyright terms: Public domain W3C validator