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 1085
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 919. (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 1083 . 2 wff (𝜑𝜓𝜒)
51, 2wo 844 . . 3 wff (𝜑𝜓)
65, 3wo 844 . 2 wff ((𝜑𝜓) ∨ 𝜒)
74, 6wb 209 1 wff ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∨ 𝜒))
Colors of variables: wff setvar class
This definition is referenced by:  3orass  1087  3orrot  1089  3ioran  1103  3ianor  1104  3orbi123i  1153  3ori  1421  3jao  1422  mpjao3danOLD  1429  3orbi123d  1432  3orim123d  1441  3or6  1444  cadan  1611  nf3or  1907  eueq3  3688  sspsstri  4065  eltpg  4608  rextpg  4620  tppreqb  4722  somo  5497  ordtri1  6211  ordeleqon  7497  bropopvvv  7781  soxp  7819  swoso  8318  en3lplem2  9073  cflim2  9683  entric  9977  entri2  9978  psslinpr  10451  ssxr  10708  relin01  11162  elznn0nn  11992  nn01to3  12338  xrnemnf  12509  xrnepnf  12510  xrsupss  12699  xrinfmss  12700  swrdnd  14016  swrdnnn0nd  14018  swrdnd0  14019  cshwshashlem1  16429  tosso  17646  pmltpc  24061  dyaddisj  24207  legso  26400  lnhl  26416  cgracol  26629  colinearalg  26711  1to3vfriswmgr  28072  3o1cs  30240  3o2cs  30241  3o3cs  30242  fzone1  30538  tlt3  30667  cycpmco2  30811  3orel3  33003  3pm3.2ni  33004  3orit  33006  soseq  33157  nosepdmlem  33248  wl-df2-3mintru2  34848  mblfinlem2  35044  ts3or1  35540  ts3or2  35541  ts3or3  35542  3orrabdioph  39645  frege114d  40380  df3or2  40390  andi3or  40649  uneqsn  40650  clsk1indlem3  40670  sbc3or  41163  en3lplem2VD  41475  3orbi123VD  41481  sbc3orgVD  41482  sbcoreleleqVD  41490  el1fzopredsuc  43813  even3prm2  44168  reorelicc  45055
  Copyright terms: Public domain W3C validator