MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-3or Structured version   Unicode version

Definition df-3or 969
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 524. (Contributed by NM, 8-Apr-1994.)
Assertion
Ref Expression
df-3or  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ( ph  \/  ps )  \/  ch ) )

Detailed syntax breakdown of Definition df-3or
StepHypRef Expression
1 wph . . 3  wff  ph
2 wps . . 3  wff  ps
3 wch . . 3  wff  ch
41, 2, 3w3o 967 . 2  wff  ( ph  \/  ps  \/  ch )
51, 2wo 368 . . 3  wff  ( ph  \/  ps )
65, 3wo 368 . 2  wff  ( (
ph  \/  ps )  \/  ch )
74, 6wb 184 1  wff  ( (
ph  \/  ps  \/  ch )  <->  ( ( ph  \/  ps )  \/  ch ) )
Colors of variables: wff setvar class
This definition is referenced by:  3orass  971  3orrot  974  3anor  984  3ioran  986  3orbi123i  1181  3ori  1283  3jao  1284  mpjao3dan  1290  3orbi123d  1293  3orim123d  1302  3or6  1305  cadan  1438  cadanOLD  1439  nf3or  1878  eueq3  3273  sspsstri  3601  eltpg  4064  rextpg  4074  tppreqb  4163  somo  4829  ordtri1  4906  ordtri3  4909  ordeleqon  6597  bropopvvv  6855  soxp  6888  swoso  7334  en3lplem2  8023  cflim2  8634  entric  8923  entri2  8924  psslinpr  9400  ssxr  9645  relin01  10068  nnnegz  10858  elznn0nn  10869  nn01to3  11166  xrnemnf  11319  xrnepnf  11320  xrsupss  11491  xrinfmss  11492  swrdnd  12609  cshwshashlem1  14429  tosso  15514  pmltpc  21592  dyaddisj  21735  legso  23707  colinearalg  23884  clwwlknprop  24436  2wlkonot3v  24539  2spthonot3v  24540  1to3vfriswmgra  24671  3o1cs  27033  3o2cs  27034  3o3cs  27035  tlt3  27303  3orel3  28552  3pm3.2ni  28553  3orit  28555  soseq  28899  nobnddown  29026  mblfinlem2  29618  ts3or1  30153  ts3or2  30154  ts3or3  30155  3orrabdioph  30310  sbc3or  32258  sbc3orgOLD  32259  en3lplem2VD  32601  3orbi123VD  32607  sbc3orgVD  32608
  Copyright terms: Public domain W3C validator