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

Definition df-3or 979
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 767. (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 977 . 2 wff (𝜑𝜓𝜒)
51, 2wo 708 . . 3 wff (𝜑𝜓)
65, 3wo 708 . 2 wff ((𝜑𝜓) ∨ 𝜒)
74, 6wb 105 1 wff ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∨ 𝜒))
Colors of variables: wff set class
This definition is referenced by:  3orass  981  3orrot  984  3ioran  993  3orbi123i  1189  3ori  1300  3jao  1301  mpjao3dan  1307  3orbi123d  1311  3orim123d  1320  3or6  1323  ecase23d  1350  hb3or  1549  eueq3dc  2913  eltpg  3639  rextpg  3648  nntri3or  6496  nntri1  6499  nnsseleq  6504  elznn0nn  9269  zleloe  9302  uzm1  9560  xrnemnf  9779  xrnepnf  9780  xrltso  9798  hashfiv01gt1  10764  prm23ge5  12266  bd3or  14666  triap  14862
  Copyright terms: Public domain W3C validator