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 1031
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 544. (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 1029 . 2 wff (𝜑𝜓𝜒)
51, 2wo 381 . . 3 wff (𝜑𝜓)
65, 3wo 381 . 2 wff ((𝜑𝜓) ∨ 𝜒)
74, 6wb 194 1 wff ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∨ 𝜒))
Colors of variables: wff setvar class
This definition is referenced by:  3orass  1033  3orrot  1036  3anor  1046  3ioran  1048  3orbi123i  1244  3ori  1379  3jao  1380  mpjao3dan  1386  3orbi123d  1389  3orim123d  1398  3or6  1401  cadan  1538  nf3or  1822  nf3orOLD  2232  eueq3  3347  sspsstri  3670  eltpg  4173  rextpg  4183  tppreqb  4276  somo  4982  ordtri1  5658  ordtri3OLD  5662  ordeleqon  6857  bropopvvv  7119  soxp  7154  swoso  7639  en3lplem2  8372  cflim2  8945  entric  9235  entri2  9236  psslinpr  9709  ssxr  9958  relin01  10403  elznn0nn  11226  nn01to3  11615  xrnemnf  11790  xrnepnf  11791  xrsupss  11969  xrinfmss  11970  swrdnd  13232  cshwshashlem1  15588  tosso  16807  pmltpc  22970  dyaddisj  23114  legso  25239  lnhl  25255  cgracol  25464  colinearalg  25535  clwwlknprop  26093  2wlkonot3v  26195  2spthonot3v  26196  1to3vfriswmgra  26327  3o1cs  28486  3o2cs  28487  3o3cs  28488  tlt3  28789  3orel3  30641  3pm3.2ni  30642  3orit  30644  soseq  30788  nobnddown  30893  mblfinlem2  32400  ts3or1  32913  ts3or2  32914  ts3or3  32915  3orrabdioph  36148  frege114d  36852  df3or2  36862  andi3or  37123  uneqsn  37124  clsk1indlem3  37144  sbc3or  37542  sbc3orgOLD  37546  en3lplem2VD  37884  3orbi123VD  37890  sbc3orgVD  37891  el1fzopredsuc  39732  1to3vfriswmgr  41431
  Copyright terms: Public domain W3C validator