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

Definition df-3or 974
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 762. (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 972 . 2  wff  ( ph  \/  ps  \/  ch )
51, 2wo 703 . . 3  wff  ( ph  \/  ps )
65, 3wo 703 . 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  976  3orrot  979  3ioran  988  3orbi123i  1184  3ori  1295  3jao  1296  mpjao3dan  1302  3orbi123d  1306  3orim123d  1315  3or6  1318  ecase23d  1345  hb3or  1542  eueq3dc  2904  eltpg  3626  rextpg  3635  nntri3or  6470  nntri1  6473  nnsseleq  6478  elznn0nn  9215  zleloe  9248  uzm1  9506  xrnemnf  9723  xrnepnf  9724  xrltso  9742  hashfiv01gt1  10705  prm23ge5  12207  bd3or  13826  triap  14023
  Copyright terms: Public domain W3C validator