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 1055
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 1053 . 2 wff (𝜑𝜓𝜒)
51, 2wo 382 . . 3 wff (𝜑𝜓)
65, 3wo 382 . 2 wff ((𝜑𝜓) ∨ 𝜒)
74, 6wb 196 1 wff ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∨ 𝜒))
Colors of variables: wff setvar class
This definition is referenced by:  3orass  1057  3orrot  1061  3anorOLD  1072  3ioran  1073  3ianor  1074  3orbi123i  1271  3ori  1428  3jao  1429  mpjao3dan  1435  3orbi123d  1438  3orim123d  1447  3or6  1450  cadan  1588  nf3or  1875  nf3orOLD  2281  eueq3  3414  sspsstri  3742  eltpg  4259  rextpg  4269  tppreqb  4368  somo  5098  ordtri1  5794  ordtri3OLD  5798  ordeleqon  7030  bropopvvv  7300  soxp  7335  swoso  7820  en3lplem2  8550  cflim2  9123  entric  9417  entri2  9418  psslinpr  9891  ssxr  10145  relin01  10590  elznn0nn  11429  nn01to3  11819  xrnemnf  11989  xrnepnf  11990  xrsupss  12177  xrinfmss  12178  swrdnd  13478  cshwshashlem1  15849  tosso  17083  pmltpc  23265  dyaddisj  23410  legso  25539  lnhl  25555  cgracol  25764  colinearalg  25835  1to3vfriswmgr  27260  3o1cs  29437  3o2cs  29438  3o3cs  29439  tlt3  29793  3orel3  31719  3pm3.2ni  31720  3orit  31722  soseq  31879  nosepdmlem  31958  mblfinlem2  33577  ts3or1  34090  ts3or2  34091  ts3or3  34092  3orrabdioph  37664  frege114d  38367  df3or2  38377  andi3or  38637  uneqsn  38638  clsk1indlem3  38658  sbc3or  39055  sbc3orgOLD  39059  en3lplem2VD  39393  3orbi123VD  39399  sbc3orgVD  39400  el1fzopredsuc  41660  even3prm2  41953
  Copyright terms: Public domain W3C validator