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 1080
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 915. (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 1078 . 2 wff (𝜑𝜓𝜒)
51, 2wo 841 . . 3 wff (𝜑𝜓)
65, 3wo 841 . 2 wff ((𝜑𝜓) ∨ 𝜒)
74, 6wb 207 1 wff ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∨ 𝜒))
Colors of variables: wff setvar class
This definition is referenced by:  3orass  1082  3orrot  1084  3ioran  1098  3ianor  1099  3orbi123i  1148  3ori  1416  3jao  1417  mpjao3dan  1423  3orbi123d  1426  3orim123d  1435  3or6  1438  cadan  1601  nf3or  1897  eueq3  3701  sspsstri  4078  eltpg  4617  rextpg  4629  tppreqb  4732  somo  5504  ordtri1  6218  ordeleqon  7491  bropopvvv  7776  soxp  7814  swoso  8312  en3lplem2  9065  cflim2  9674  entric  9968  entri2  9969  psslinpr  10442  ssxr  10699  relin01  11153  elznn0nn  11984  nn01to3  12330  xrnemnf  12502  xrnepnf  12503  xrsupss  12692  xrinfmss  12693  swrdnd  14006  swrdnnn0nd  14008  swrdnd0  14009  cshwshashlem1  16419  tosso  17636  pmltpc  23980  dyaddisj  24126  legso  26313  lnhl  26329  cgracol  26542  colinearalg  26624  1to3vfriswmgr  27987  3o1cs  30155  3o2cs  30156  3o3cs  30157  fzone1  30450  tlt3  30580  cycpmco2  30703  3orel3  32840  3pm3.2ni  32841  3orit  32843  soseq  32994  nosepdmlem  33085  mblfinlem2  34812  ts3or1  35314  ts3or2  35315  ts3or3  35316  3orrabdioph  39260  frege114d  39983  df3or2  39993  andi3or  40252  uneqsn  40253  clsk1indlem3  40273  sbc3or  40746  en3lplem2VD  41058  3orbi123VD  41064  sbc3orgVD  41065  sbcoreleleqVD  41073  el1fzopredsuc  43406  even3prm2  43731  reorelicc  44595
  Copyright terms: Public domain W3C validator