New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-3or GIF 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 wff φ
2 wps . . 3 wff ψ
3 wch . . 3 wff χ
41, 2, 3w3o 933 . 2 wff (φ ψ χ)
51, 2wo 357 . . 3 wff (φ ψ)
65, 3wo 357 . 2 wff ((φ ψ) χ)
74, 6wb 176 1 wff ((φ ψ χ) ↔ ((φ ψ) χ))
 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