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  2942  sotric  4340  sotrieq  4341  isso2i  4346  ordzsl  4636  soxp  6228  wemapso2lem  7265  rankxpsuc  7552  tcrank  7554  cardlim  7605  cardaleph  7716  grur1  8442  elnnz  10034  elznn0  10038  elznn  10039  elxr  10458  xrrebnd  10497  xaddf  10551  xrinfmss  10628  eliccioo  23115  xrdifh  23273  3orel1  24061  dfso2  24111  dfon2lem5  24143  dfon2lem6  24144  nofv  24311  nobndup  24354  dvreasin  24923  ecase13d  26222  elicc3  26228  3ornot23VD  28623  4atlem3a  29786  4atlem3b  29787
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