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  3628  rextpg  3637  nntri3or  6472  nntri1  6475  nnsseleq  6480  elznn0nn  9226  zleloe  9259  uzm1  9517  xrnemnf  9734  xrnepnf  9735  xrltso  9753  hashfiv01gt1  10716  prm23ge5  12218  bd3or  13864  triap  14061
  Copyright terms: Public domain W3C validator