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

Definition df-3or 886
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 684. (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 884 . 2  wff  ( ph  \/  ps  \/  ch )
51, 2wo 629 . . 3  wff  ( ph  \/  ps )
65, 3wo 629 . 2  wff  ( (
ph  \/  ps )  \/  ch )
74, 6wb 98 1  wff  ( (
ph  \/  ps  \/  ch )  <->  ( ( ph  \/  ps )  \/  ch ) )
Colors of variables: wff set class
This definition is referenced by:  3orass  888  3orrot  891  3ioran  900  3orbi123i  1094  3ori  1195  3jao  1196  mpjao3dan  1202  3orbi123d  1206  3orim123d  1215  3or6  1218  ecase23d  1240  hb3or  1441  eueq3dc  2715  eltpg  3416  rextpg  3424  nntri3or  6072  nntri1  6074  nnsseleq  6079  elznn0nn  8259  zleloe  8292  uzm1  8503  xrnemnf  8699  xrnepnf  8700  xrltso  8717  bd3or  9949
  Copyright terms: Public domain W3C validator