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

Definition df-3or 969
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 967 . 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  971  3orrot  974  3ioran  983  3orbi123i  1179  3ori  1290  3jao  1291  mpjao3dan  1297  3orbi123d  1301  3orim123d  1310  3or6  1313  ecase23d  1340  hb3or  1537  eueq3dc  2899  eltpg  3620  rextpg  3629  nntri3or  6457  nntri1  6460  nnsseleq  6465  elznn0nn  9201  zleloe  9234  uzm1  9492  xrnemnf  9709  xrnepnf  9710  xrltso  9728  hashfiv01gt1  10691  prm23ge5  12192  bd3or  13671  triap  13868
  Copyright terms: Public domain W3C validator