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

Definition df-3or 874
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 671. (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 872 . 2 wff (φ ψ χ)
51, 2wo 616 . . 3 wff (φ ψ)
65, 3wo 616 . 2 wff ((φ ψ) χ)
74, 6wb 98 1 wff ((φ ψ χ) ↔ ((φ ψ) χ))
Colors of variables: wff set class
This definition is referenced by:  3orass  876  3orrot  879  3ioran  888  3orbi123i  1080  3ori  1181  3jao  1182  3orbi123d  1191  3orim123d  1200  3or6  1203  ecase23d  1225  hb3or  1423  eueq3dc  2692  eltpg  3390  rextpg  3398  nntri3or  5987  nntri1  5989  bd3or  7203
  Copyright terms: Public domain W3C validator