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

Definition df-3or 975
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 973 . 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  977  3orrot  980  3anor  990  3ioran  992  3orbi123i  1187  3ori  1289  3jao  1290  mpjao3dan  1296  3orbi123d  1299  3orim123d  1308  3or6  1311  cadan  1447  nf3or  1922  eueq3  3260  sspsstri  3591  eltpg  4056  rextpg  4066  tppreqb  4156  somo  4824  ordtri1  4901  ordtri3  4904  ordeleqon  6609  bropopvvv  6865  soxp  6898  swoso  7344  en3lplem2  8035  cflim2  8646  entric  8935  entri2  8936  psslinpr  9412  ssxr  9657  relin01  10084  elznn0nn  10885  nn01to3  11186  xrnemnf  11339  xrnepnf  11340  xrsupss  11511  xrinfmss  11512  swrdnd  12639  cshwshashlem1  14562  tosso  15645  pmltpc  21840  dyaddisj  21983  legso  23963  colinearalg  24191  clwwlknprop  24750  2wlkonot3v  24853  2spthonot3v  24854  1to3vfriswmgra  24985  3o1cs  27347  3o2cs  27348  3o3cs  27349  tlt3  27631  3orel3  29067  3pm3.2ni  29068  3orit  29070  soseq  29310  nobnddown  29437  mblfinlem2  30028  ts3or1  30536  ts3or2  30537  ts3or3  30538  3orrabdioph  30693  sbc3or  33170  sbc3orgOLD  33171  en3lplem2VD  33512  3orbi123VD  33518  sbc3orgVD  33519
  Copyright terms: Public domain W3C validator