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

Definition df-3or 981
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 768. (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 979 . 2 wff (𝜑𝜓𝜒)
51, 2wo 709 . . 3 wff (𝜑𝜓)
65, 3wo 709 . 2 wff ((𝜑𝜓) ∨ 𝜒)
74, 6wb 105 1 wff ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∨ 𝜒))
Colors of variables: wff set class
This definition is referenced by:  3orass  983  3orrot  986  3ioran  995  3orbi123i  1191  3ori  1311  3jao  1312  mpjao3dan  1318  3orbi123d  1322  3orim123d  1331  3or6  1334  ecase23d  1361  hb3or  1560  eueq3dc  2926  eltpg  3652  rextpg  3661  nntri3or  6512  nntri1  6515  nnsseleq  6520  elznn0nn  9285  zleloe  9318  uzm1  9576  xrnemnf  9795  xrnepnf  9796  xrltso  9814  hashfiv01gt1  10780  prm23ge5  12282  bd3or  14965  triap  15162
  Copyright terms: Public domain W3C validator