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

Definition df-3or 885
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 683. (Contributed by NM, 8-Apr-1994.)
Assertion
Ref Expression
df-3or

Detailed syntax breakdown of Definition df-3or
StepHypRef Expression
1 wph . . 3
2 wps . . 3
3 wch . . 3
41, 2, 3w3o 883 . 2
51, 2wo 628 . . 3
65, 3wo 628 . 2
74, 6wb 98 1
Colors of variables: wff set class
This definition is referenced by:  3orass  887  3orrot  890  3ioran  899  3orbi123i  1093  3ori  1194  3jao  1195  mpjao3dan  1201  3orbi123d  1205  3orim123d  1214  3or6  1217  ecase23d  1239  hb3or  1438  eueq3dc  2709  eltpg  3407  rextpg  3415  nntri3or  6011  nntri1  6013  elznn0nn  8015  zleloe  8048  uzm1  8259  xrnemnf  8449  xrnepnf  8450  xrltso  8467  bd3or  9264
  Copyright terms: Public domain W3C validator