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

Theorem 3orass 974
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 972 . 2  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ( ph  \/  ps )  \/  ch ) )
2 orass 522 . 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 366    \/ w3o 970
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 368  df-3or 972
This theorem is referenced by:  3orrot  977  3orcoma  979  3orcomb  981  3mix1  1163  ecase23d  1330  3bior1fd  1332  cador  1461  moeq3  3273  sotric  4815  sotrieq  4816  isso2i  4821  ordzsl  6653  soxp  6886  wemapsolem  7967  rankxpsuc  8291  tcrank  8293  cardlim  8344  cardaleph  8461  grur1  9187  elnnz  10870  elznn0  10875  elznn  10876  elxr  11328  xrrebnd  11372  xaddf  11426  xrinfmss  11504  ssnn0fi  12076  hashv01gt1  12400  hashtpg  12507  swrdnd2  12649  tgldimor  24094  xrdifh  27825  eliccioo  27861  orngsqr  28029  elzdif0  28195  qqhval2lem  28196  3orel1  29328  dfso2  29424  socnv  29435  dfon2lem5  29459  dfon2lem6  29460  nofv  29657  nobndup  29700  wl-exeq  30227  dvasin  30343  ecase13d  30371  elicc3  30375  3ornot23VD  34047  4atlem3a  35718  4atlem3b  35719
  Copyright terms: Public domain W3C validator