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

Definition df-3or 964
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 757. (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 962 . 2 wff (𝜑𝜓𝜒)
51, 2wo 698 . . 3 wff (𝜑𝜓)
65, 3wo 698 . 2 wff ((𝜑𝜓) ∨ 𝜒)
74, 6wb 104 1 wff ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∨ 𝜒))
Colors of variables: wff set class
This definition is referenced by:  3orass  966  3orrot  969  3ioran  978  3orbi123i  1172  3ori  1282  3jao  1283  mpjao3dan  1289  3orbi123d  1293  3orim123d  1302  3or6  1305  ecase23d  1332  hb3or  1529  eueq3dc  2886  eltpg  3606  rextpg  3615  nntri3or  6443  nntri1  6446  nnsseleq  6451  elznn0nn  9187  zleloe  9220  uzm1  9475  xrnemnf  9691  xrnepnf  9692  xrltso  9710  hashfiv01gt1  10668  prm23ge5  12155  bd3or  13501  triap  13697
  Copyright terms: Public domain W3C validator