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

Definition df-3or 972
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 522. (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 970 . 2  wff  ( ph  \/  ps  \/  ch )
51, 2wo 366 . . 3  wff  ( ph  \/  ps )
65, 3wo 366 . 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  974  3orrot  977  3anor  987  3ioran  989  3orbi123i  1184  3ori  1286  3jao  1287  mpjao3dan  1293  3orbi123d  1296  3orim123d  1305  3or6  1308  cadan  1466  nf3or  1944  eueq3  3199  sspsstri  3520  eltpg  3986  rextpg  3996  tppreqb  4085  somo  4748  ordtri1  4825  ordtri3  4828  ordeleqon  6523  bropopvvv  6779  soxp  6812  swoso  7260  en3lplem2  7946  cflim2  8556  entric  8845  entri2  8846  psslinpr  9320  ssxr  9565  relin01  9994  elznn0nn  10795  nn01to3  11094  xrnemnf  11249  xrnepnf  11250  xrsupss  11421  xrinfmss  11422  swrdnd  12568  cshwshashlem1  14582  tosso  15783  pmltpc  21947  dyaddisj  22090  legso  24105  colinearalg  24334  clwwlknprop  24893  2wlkonot3v  24996  2spthonot3v  24997  1to3vfriswmgra  25128  3o1cs  27486  3o2cs  27487  3o3cs  27488  tlt3  27806  3orel3  29255  3pm3.2ni  29256  3orit  29258  soseq  29499  nobnddown  29626  mblfinlem2  30217  ts3or1  30726  ts3or2  30727  ts3or3  30728  3orrabdioph  30882  sbc3or  33635  sbc3orgOLD  33639  en3lplem2VD  33990  3orbi123VD  33996  sbc3orgVD  33997
  Copyright terms: Public domain W3C validator