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

Definition df-3or 886
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 684. (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 884 . 2 wff (𝜑𝜓𝜒)
51, 2wo 629 . . 3 wff (𝜑𝜓)
65, 3wo 629 . 2 wff ((𝜑𝜓) ∨ 𝜒)
74, 6wb 98 1 wff ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∨ 𝜒))
Colors of variables: wff set class
This definition is referenced by:  3orass  888  3orrot  891  3ioran  900  3orbi123i  1094  3ori  1195  3jao  1196  mpjao3dan  1202  3orbi123d  1206  3orim123d  1215  3or6  1218  ecase23d  1240  hb3or  1441  eueq3dc  2712  eltpg  3413  rextpg  3421  nntri3or  6050  nntri1  6052  nnsseleq  6057  elznn0nn  8222  zleloe  8255  uzm1  8466  xrnemnf  8657  xrnepnf  8658  xrltso  8675  bd3or  9813
  Copyright terms: Public domain W3C validator