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

Theorem 3orass 968
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 966 . 2  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ( ph  \/  ps )  \/  ch ) )
2 orass 524 . 2  |-  ( ( ( ph  \/  ps )  \/  ch )  <->  (
ph  \/  ( ps  \/  ch ) ) )
31, 2bitri 249 1  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ph  \/  ( ps  \/  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    \/ wo 368    \/ w3o 964
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-or 370  df-3or 966
This theorem is referenced by:  3orrot  971  3orcoma  973  3orcomb  975  3mix1  1157  ecase23d  1323  3bior1fd  1325  cador  1433  moeq3  3219  sotric  4751  sotrieq  4752  isso2i  4757  ordzsl  6542  soxp  6771  wemapsolem  7851  rankxpsuc  8176  tcrank  8178  cardlim  8229  cardaleph  8346  grur1  9074  elnnz  10743  elznn0  10748  elznn  10749  elxr  11183  xrrebnd  11227  xaddf  11281  xrinfmss  11359  hashv01gt1  12203  hashtpg  12274  swrdvalodm2  12421  swrdvalodm  12422  tgldimor  23059  xrdifh  26190  eliccioo  26226  orngsqr  26392  elzdif0  26529  qqhval2lem  26530  3orel1  27486  dfso2  27684  socnv  27695  dfon2lem5  27720  dfon2lem6  27721  nofv  27918  nobndup  27961  wl-exeq  28487  dvasin  28604  ecase13d  28632  elicc3  28636  ssnn0fi  30870  3ornot23VD  31865  4atlem3a  33523  4atlem3b  33524
  Copyright terms: Public domain W3C validator