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

Definition df-3or 948
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 741. (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 946 . 2 wff (𝜑𝜓𝜒)
51, 2wo 682 . . 3 wff (𝜑𝜓)
65, 3wo 682 . 2 wff ((𝜑𝜓) ∨ 𝜒)
74, 6wb 104 1 wff ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∨ 𝜒))
Colors of variables: wff set class
This definition is referenced by:  3orass  950  3orrot  953  3ioran  962  3orbi123i  1156  3ori  1263  3jao  1264  mpjao3dan  1270  3orbi123d  1274  3orim123d  1283  3or6  1286  ecase23d  1313  hb3or  1513  eueq3dc  2831  eltpg  3539  rextpg  3547  nntri3or  6357  nntri1  6360  nnsseleq  6365  elznn0nn  9026  zleloe  9059  uzm1  9312  xrnemnf  9519  xrnepnf  9520  xrltso  9537  hashfiv01gt1  10483  bd3or  12923  triap  13120
  Copyright terms: Public domain W3C validator