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 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 511. (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 358 . . 3  wff  ( ph  \/  ps )
65, 3wo 358 . 2  wff  ( (
ph  \/  ps )  \/  ch )
74, 6wb 177 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  1398  nf3or  1855  eueq3  3069  sspsstri  3409  eltpg  3811  rextpg  3820  tppreqb  3899  somo  4497  ordtri1  4574  ordtri3  4577  ordeleqon  4728  bropopvvv  6385  soxp  6418  swoso  6895  en3lplem2  7627  cflim2  8099  entric  8388  entri2  8389  psslinpr  8864  ssxr  9101  nnnegz  10241  elznn0nn  10251  xrnemnf  10674  xrnepnf  10675  xrsupss  10843  xrinfmss  10844  tosso  14420  pmltpc  19300  dyaddisj  19441  3o1cs  23906  3o2cs  23907  3o3cs  23908  3orel3  25119  3pm3.2ni  25120  3orit  25122  relin01  25147  soseq  25468  nobnddown  25569  colinearalg  25753  mblfinlem  26143  3orrabdioph  26732  swrdnd  28001  2wlkonot3v  28072  2spthonot3v  28073  1to3vfriswmgra  28111  sbc3org  28327  en3lplem2VD  28665  3orbi123VD  28671  sbc3orgVD  28672
  Copyright terms: Public domain W3C validator