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 1088
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 922. (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 1086 . 2 wff (𝜑𝜓𝜒)
51, 2wo 848 . . 3 wff (𝜑𝜓)
65, 3wo 848 . 2 wff ((𝜑𝜓) ∨ 𝜒)
74, 6wb 206 1 wff ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∨ 𝜒))
Colors of variables: wff setvar class
This definition is referenced by:  3orass  1090  3orrot  1092  3ioran  1106  3ianor  1107  3orbi123i  1157  3ori  1426  3jao  1427  3jaob  1428  3orbi123d  1437  3orim123d  1446  3or6  1449  3orel3  1488  3pm3.2ni  1490  cadan  1609  nf3or  1905  eueq3  3717  sspsstri  4105  eltpg  4686  rextpg  4699  tppreqb  4805  somo  5631  ordtri1  6417  ordeleqon  7802  bropopvvv  8115  soxp  8154  soseq  8184  swoso  8779  fsetexb  8904  en3lplem2  9653  cflim2  10303  entric  10597  entri2  10598  psslinpr  11071  ssxr  11330  relin01  11787  elznn0nn  12627  nn01to3  12983  xrnemnf  13159  xrnepnf  13160  xrsupss  13351  xrinfmss  13352  swrdnd  14692  swrdnnn0nd  14694  swrdnd0  14695  cshwshashlem1  17133  tosso  18464  pmltpc  25485  dyaddisj  25631  nosepdmlem  27728  mulsproplem13  28154  mulsproplem14  28155  legso  28607  lnhl  28623  cgracol  28836  colinearalg  28925  1to3vfriswmgr  30299  3o1cs  32480  3o2cs  32481  3o3cs  32482  3unrab  32522  fzone1  32802  tlt3  32960  cycpmco2  33153  3orit  35716  wl-df2-3mintru2  37486  mblfinlem2  37665  ts3or1  38160  ts3or2  38161  ts3or3  38162  3orrabdioph  42794  oneptri  43269  frege114d  43771  df3or2  43781  andi3or  44037  uneqsn  44038  clsk1indlem3  44056  sbc3or  44552  en3lplem2VD  44864  3orbi123VD  44870  sbc3orgVD  44871  sbcoreleleqVD  44879  el1fzopredsuc  47337  even3prm2  47706  usgrexmpl2nb1  47991  usgrexmpl2nb4  47994  reorelicc  48631
  Copyright terms: Public domain W3C validator