MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-3or Structured version   Visualization version   GIF version

Definition df-3or 1101
Description: Define disjunction ('or') of three 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 936. (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 1099 . 2 wff (𝜑𝜓𝜒)
51, 2wo 865 . . 3 wff (𝜑𝜓)
65, 3wo 865 . 2 wff ((𝜑𝜓) ∨ 𝜒)
74, 6wb 197 1 wff ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∨ 𝜒))
Colors of variables: wff setvar class
This definition is referenced by:  3orass  1103  3orrot  1105  3anorOLD  1123  3ioran  1124  3ianor  1125  3orbi123i  1188  3ori  1541  3jao  1542  3jaoOLD  1543  mpjao3dan  1549  3orbi123d  1552  3orim123d  1561  3or6  1564  cadan  1703  nf3or  1997  nf3orOLD  2419  eueq3  3579  sspsstri  3907  eltpg  4419  rextpg  4429  tppreqb  4526  somo  5266  ordtri1  5969  ordeleqon  7214  bropopvvv  7485  soxp  7520  swoso  8008  en3lplem2  8751  cflim2  9366  entric  9660  entri2  9661  psslinpr  10134  ssxr  10388  relin01  10833  elznn0nn  11653  nn01to3  11996  xrnemnf  12163  xrnepnf  12164  xrsupss  12353  xrinfmss  12354  swrdnd  13652  cshwshashlem1  16010  tosso  17237  pmltpc  23427  dyaddisj  23573  legso  25704  lnhl  25720  cgracol  25929  colinearalg  26000  1to3vfriswmgr  27451  3o1cs  29633  3o2cs  29634  3o3cs  29635  tlt3  29986  3orel3  31910  3pm3.2ni  31911  3orit  31913  soseq  32070  nosepdmlem  32149  mblfinlem2  33755  ts3or1  34265  ts3or2  34266  ts3or3  34267  3orrabdioph  37843  frege114d  38544  df3or2  38554  andi3or  38814  uneqsn  38815  clsk1indlem3  38835  sbc3or  39230  sbc3orgOLD  39234  en3lplem2VD  39567  3orbi123VD  39573  sbc3orgVD  39574  el1fzopredsuc  41904  even3prm2  42197
  Copyright terms: Public domain W3C validator