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 1032
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 545. (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 1030 . 2 wff (𝜑𝜓𝜒)
51, 2wo 382 . . 3 wff (𝜑𝜓)
65, 3wo 382 . 2 wff ((𝜑𝜓) ∨ 𝜒)
74, 6wb 195 1 wff ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∨ 𝜒))
Colors of variables: wff setvar class
This definition is referenced by:  3orass  1034  3orrot  1037  3anor  1047  3ioran  1049  3orbi123i  1245  3ori  1380  3jao  1381  mpjao3dan  1387  3orbi123d  1390  3orim123d  1399  3or6  1402  cadan  1539  nf3or  1823  nf3orOLD  2233  eueq3  3348  sspsstri  3671  eltpg  4174  rextpg  4184  tppreqb  4277  somo  4993  ordtri1  5673  ordtri3OLD  5677  ordeleqon  6880  bropopvvv  7142  soxp  7177  swoso  7662  en3lplem2  8395  cflim2  8968  entric  9258  entri2  9259  psslinpr  9732  ssxr  9986  relin01  10431  elznn0nn  11268  nn01to3  11657  xrnemnf  11827  xrnepnf  11828  xrsupss  12011  xrinfmss  12012  swrdnd  13284  cshwshashlem1  15640  tosso  16859  pmltpc  23026  dyaddisj  23170  legso  25294  lnhl  25310  cgracol  25519  colinearalg  25590  clwwlknprop  26300  2wlkonot3v  26402  2spthonot3v  26403  1to3vfriswmgra  26534  3o1cs  28693  3o2cs  28694  3o3cs  28695  tlt3  28996  3orel3  30848  3pm3.2ni  30849  3orit  30851  soseq  30995  nobnddown  31100  mblfinlem2  32617  ts3or1  33130  ts3or2  33131  ts3or3  33132  3orrabdioph  36365  frege114d  37069  df3or2  37079  andi3or  37340  uneqsn  37341  clsk1indlem3  37361  sbc3or  37759  sbc3orgOLD  37763  en3lplem2VD  38101  3orbi123VD  38107  sbc3orgVD  38108  el1fzopredsuc  39948  1to3vfriswmgr  41450
  Copyright terms: Public domain W3C validator