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

Theorem 3orass 940
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 938 . 2  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ( ph  \/  ps )  \/  ch ) )
2 orass 512 . 2  |-  ( ( ( ph  \/  ps )  \/  ch )  <->  (
ph  \/  ( ps  \/  ch ) ) )
31, 2bitri 242 1  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ph  \/  ( ps  \/  ch ) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    \/ wo 359    \/ w3o 936
This theorem is referenced by:  3orrot  943  3orcoma  945  3orcomb  947  3mix1  1127  ecase23d  1288  3bior1fd  1290  cador  1401  moeq3  3112  sotric  4530  sotrieq  4531  isso2i  4536  ordzsl  4826  soxp  6460  wemapso2lem  7520  rankxpsuc  7807  tcrank  7809  cardlim  7860  cardaleph  7971  grur1  8696  elnnz  10293  elznn0  10297  elznn  10298  elxr  10717  xrrebnd  10757  xaddf  10811  xrinfmss  10889  hashv01gt1  11630  hashtpg  11692  xrdifh  24144  eliccioo  24178  ofldsqr  24241  elzdif0  24365  qqhval2lem  24366  3orel1  25165  dfso2  25378  socnv  25389  dfon2lem5  25415  dfon2lem6  25416  nofv  25613  nobndup  25656  wl-exeq  26235  dvreasin  26291  ecase13d  26317  elicc3  26321  swrdvalodm2  28189  swrdvalodm  28190  3ornot23VD  28960  4atlem3a  30395  4atlem3b  30396
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 179  df-or 361  df-3or 938
  Copyright terms: Public domain W3C validator