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

Definition df-3or 937
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 935 . 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  939  3orrot  942  3anor  950  3ioran  952  3orbi123i  1143  3ori  1244  3jao  1245  3orbi123d  1253  3orim123d  1262  3or6  1265  cadan  1384  nf3or  1777  eueq3  2943  sspsstri  3281  eltpg  3679  rextpg  3688  somo  4349  ordtri1  4426  ordtri3  4429  ordeleqon  4581  soxp  6191  swoso  6688  en3lplem2  7414  cflim2  7886  entric  8176  entri2  8177  psslinpr  8652  ssxr  8889  nnnegz  10024  elznn0nn  10034  xrnemnf  10457  xrnepnf  10458  xrsupss  10623  xrinfmss  10624  tosso  14138  pmltpc  18806  dyaddisj  18947  3orel3  23469  3pm3.2ni  23470  3orit  23472  relin01  23494  soseq  23657  axfelem10  23758  colinearalg  23947  anddi2  24341  fixpc  24494  3orrabdioph  26264  sbc3org  27568  en3lplem2VD  27890  3orbi123VD  27896  sbc3orgVD  27897
  Copyright terms: Public domain W3C validator