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

Definition df-3or 938
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 512. (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 936 . 2  wff  ( ph  \/  ps  \/  ch )
51, 2wo 359 . . 3  wff  ( ph  \/  ps )
65, 3wo 359 . 2  wff  ( (
ph  \/  ps )  \/  ch )
74, 6wb 178 1  wff  ( (
ph  \/  ps  \/  ch )  <->  ( ( ph  \/  ps )  \/  ch ) )
Colors of variables: wff set class
This definition is referenced by:  3orass  940  3orrot  943  3anor  951  3ioran  953  3orbi123i  1144  3ori  1245  3jao  1246  3orbi123d  1254  3orim123d  1263  3or6  1266  cadan  1402  nf3or  1860  eueq3  3111  sspsstri  3451  eltpg  3853  rextpg  3862  tppreqb  3941  somo  4540  ordtri1  4617  ordtri3  4620  ordeleqon  4772  bropopvvv  6429  soxp  6462  swoso  6939  en3lplem2  7674  cflim2  8148  entric  8437  entri2  8438  psslinpr  8913  ssxr  9150  nnnegz  10290  elznn0nn  10300  xrnemnf  10723  xrnepnf  10724  xrsupss  10892  xrinfmss  10893  tosso  14470  pmltpc  19352  dyaddisj  19493  3o1cs  23958  3o2cs  23959  3o3cs  23960  3orel3  25171  3pm3.2ni  25172  3orit  25174  relin01  25199  soseq  25534  nobnddown  25661  colinearalg  25854  mblfinlem2  26256  3orrabdioph  26856  elovmpt3rab1  28107  swrdnd  28216  cshwssizelem2  28315  2wlkonot3v  28407  2spthonot3v  28408  1to3vfriswmgra  28471  sbc3org  28690  en3lplem2VD  29030  3orbi123VD  29036  sbc3orgVD  29037
  Copyright terms: Public domain W3C validator