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

Definition df-3or 931
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 725. (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 929 . 2  wff  ( ph  \/  ps  \/  ch )
51, 2wo 670 . . 3  wff  ( ph  \/  ps )
65, 3wo 670 . 2  wff  ( (
ph  \/  ps )  \/  ch )
74, 6wb 104 1  wff  ( (
ph  \/  ps  \/  ch )  <->  ( ( ph  \/  ps )  \/  ch ) )
Colors of variables: wff set class
This definition is referenced by:  3orass  933  3orrot  936  3ioran  945  3orbi123i  1139  3ori  1246  3jao  1247  mpjao3dan  1253  3orbi123d  1257  3orim123d  1266  3or6  1269  ecase23d  1296  hb3or  1496  eueq3dc  2811  eltpg  3516  rextpg  3524  nntri3or  6319  nntri1  6322  nnsseleq  6327  elznn0nn  8920  zleloe  8953  uzm1  9206  xrnemnf  9405  xrnepnf  9406  xrltso  9423  hashfiv01gt1  10369  bd3or  12608  triap  12808
  Copyright terms: Public domain W3C validator