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

Definition df-3or 946
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 739. (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 944 . 2 wff (𝜑𝜓𝜒)
51, 2wo 680 . . 3 wff (𝜑𝜓)
65, 3wo 680 . 2 wff ((𝜑𝜓) ∨ 𝜒)
74, 6wb 104 1 wff ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∨ 𝜒))
Colors of variables: wff set class
This definition is referenced by:  3orass  948  3orrot  951  3ioran  960  3orbi123i  1154  3ori  1261  3jao  1262  mpjao3dan  1268  3orbi123d  1272  3orim123d  1281  3or6  1284  ecase23d  1311  hb3or  1511  eueq3dc  2829  eltpg  3537  rextpg  3545  nntri3or  6355  nntri1  6358  nnsseleq  6363  elznn0nn  9022  zleloe  9055  uzm1  9308  xrnemnf  9515  xrnepnf  9516  xrltso  9533  hashfiv01gt1  10479  bd3or  12861  triap  13058
  Copyright terms: Public domain W3C validator