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

Definition df-3or 923
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 717. (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 921 . 2 wff (𝜑𝜓𝜒)
51, 2wo 662 . . 3 wff (𝜑𝜓)
65, 3wo 662 . 2 wff ((𝜑𝜓) ∨ 𝜒)
74, 6wb 103 1 wff ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∨ 𝜒))
Colors of variables: wff set class
This definition is referenced by:  3orass  925  3orrot  928  3ioran  937  3orbi123i  1131  3ori  1234  3jao  1235  mpjao3dan  1241  3orbi123d  1245  3orim123d  1254  3or6  1257  ecase23d  1284  hb3or  1484  eueq3dc  2780  eltpg  3473  rextpg  3481  nntri3or  6210  nntri1  6213  nnsseleq  6218  elznn0nn  8700  zleloe  8733  uzm1  8984  xrnemnf  9183  xrnepnf  9184  xrltso  9201  hashfiv01gt1  10090  bd3or  11189
  Copyright terms: Public domain W3C validator