ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-3or Unicode version

Definition df-3or 897
Description: Define disjunction ('or') of 3 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 694. (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 895 . 2  wff  ( ph  \/  ps  \/  ch )
51, 2wo 639 . . 3  wff  ( ph  \/  ps )
65, 3wo 639 . 2  wff  ( (
ph  \/  ps )  \/  ch )
74, 6wb 102 1  wff  ( (
ph  \/  ps  \/  ch )  <->  ( ( ph  \/  ps )  \/  ch ) )
Colors of variables: wff set class
This definition is referenced by:  3orass  899  3orrot  902  3ioran  911  3orbi123i  1105  3ori  1206  3jao  1207  mpjao3dan  1213  3orbi123d  1217  3orim123d  1226  3or6  1229  ecase23d  1256  hb3or  1457  eueq3dc  2737  eltpg  3443  rextpg  3451  nntri3or  6102  nntri1  6104  nnsseleq  6109  elznn0nn  8315  zleloe  8348  uzm1  8598  xrnemnf  8799  xrnepnf  8800  xrltso  8817  bd3or  10322
  Copyright terms: Public domain W3C validator