ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-3or Structured version   GIF 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 wff φ
2 wps . . 3 wff ψ
3 wch . . 3 wff χ
41, 2, 3w3o 883 . 2 wff (φ ψ χ)
51, 2wo 628 . . 3 wff (φ ψ)
65, 3wo 628 . 2 wff ((φ ψ) χ)
74, 6wb 98 1 wff ((φ ψ χ) ↔ ((φ ψ) χ))
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  3406  rextpg  3414  nntri3or  6004  nntri1  6006  elznn0nn  7985  zleloe  8018  uzm1  8228  xrnemnf  8417  xrnepnf  8418  xrltso  8435  bd3or  8883
  Copyright terms: Public domain W3C validator