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

Theorem 3orass 937
Description: Associative law for triple disjunction. (Contributed by NM, 8-Apr-1994.)
Assertion
Ref Expression
3orass  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ph  \/  ( ps  \/  ch ) ) )

Proof of Theorem 3orass
StepHypRef Expression
1 df-3or 935 . 2  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ( ph  \/  ps )  \/  ch ) )
2 orass 510 . 2  |-  ( ( ( ph  \/  ps )  \/  ch )  <->  (
ph  \/  ( ps  \/  ch ) ) )
31, 2bitri 240 1  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ph  \/  ( ps  \/  ch ) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    \/ wo 357    \/ w3o 933
This theorem is referenced by:  3orrot  940  3orcoma  942  3orcomb  944  3mix1  1124  ecase23d  1285  cador  1381  moeq3  2955  sotric  4356  sotrieq  4357  isso2i  4362  ordzsl  4652  soxp  6244  wemapso2lem  7281  rankxpsuc  7568  tcrank  7570  cardlim  7621  cardaleph  7732  grur1  8458  elnnz  10050  elznn0  10054  elznn  10055  elxr  10474  xrrebnd  10513  xaddf  10567  xrinfmss  10644  eliccioo  23131  xrdifh  23288  3orel1  24076  dfso2  24182  dfon2lem5  24214  dfon2lem6  24215  nofv  24382  nobndup  24425  dvreasin  25026  ecase13d  26325  elicc3  26331  3bior1fd  28177  hashtpg  28217  3ornot23VD  28939  4atlem3a  30408  4atlem3b  30409
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359  df-3or 935
  Copyright terms: Public domain W3C validator