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

Definition df-3or 940
Description: Define disjunction ('or') of 3 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 938 . 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  942  3orrot  945  3anor  953  3ioran  955  3orbi123i  1146  3ori  1247  3jao  1248  3orbi123d  1256  3orim123d  1265  3or6  1268  cadan  1388  nf3or  1739  eueq3  2877  sspsstri  3198  eltpg  3580  rextpg  3589  somo  4241  ordtri1  4318  ordtri3  4321  ordeleqon  4471  soxp  6080  swoso  6577  en3lplem2  7301  cflim2  7773  entric  8061  entri2  8062  psslinpr  8535  ssxr  8772  nnnegz  9906  elznn0nn  9916  xrnemnf  10339  xrnepnf  10340  xrsupss  10505  xrinfmss  10506  tosso  13986  pmltpc  18642  dyaddisj  18783  3orel3  23234  3pm3.2ni  23235  3orit  23237  relin01  23259  soseq  23422  axfelem10  23523  colinearalg  23712  anddi2  24106  fixpc  24259  3orrabdioph  26029  sbc3org  26988  en3lplem2VD  27310  3orbi123VD  27316  sbc3orgVD  27317
  Copyright terms: Public domain W3C validator