NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-3or Unicode version

Definition df-3or 935
Description: Define disjunction ('or') of three 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 510. (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 933 . 2
51, 2wo 357 . . 3
65, 3wo 357 . 2
74, 6wb 176 1
Colors of variables: wff setvar class
This definition is referenced by:  3orass  937  3orrot  940  3anor  948  3ioran  950  3orbi123i  1141  3ori  1242  3jao  1243  3orbi123d  1251  3orim123d  1260  3or6  1263  cadan  1392  nf3or  1837  eueq3  3011  sspsstri  3371  eltpg  3769  rextpg  3778  ltfintrilem1  4465  sfin111  4536  nncdiv3lem2  6276  nncdiv3  6277
  Copyright terms: Public domain W3C validator