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

Definition df-3or 964
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 757. (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 962 . 2  wff  ( ph  \/  ps  \/  ch )
51, 2wo 698 . . 3  wff  ( ph  \/  ps )
65, 3wo 698 . 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  966  3orrot  969  3ioran  978  3orbi123i  1172  3ori  1279  3jao  1280  mpjao3dan  1286  3orbi123d  1290  3orim123d  1299  3or6  1302  ecase23d  1329  hb3or  1529  eueq3dc  2861  eltpg  3574  rextpg  3583  nntri3or  6395  nntri1  6398  nnsseleq  6403  elznn0nn  9090  zleloe  9123  uzm1  9378  xrnemnf  9592  xrnepnf  9593  xrltso  9610  hashfiv01gt1  10558  bd3or  13191  triap  13392
  Copyright terms: Public domain W3C validator