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

Theorem 3orrot 940
Description: Rotation law for triple disjunction. (Contributed by NM, 4-Apr-1995.)
Assertion
Ref Expression
3orrot  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ps  \/  ch  \/  ph ) )

Proof of Theorem 3orrot
StepHypRef Expression
1 orcom 376 . 2  |-  ( (
ph  \/  ( ps  \/  ch ) )  <->  ( ( ps  \/  ch )  \/ 
ph ) )
2 3orass 937 . 2  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ph  \/  ( ps  \/  ch ) ) )
3 df-3or 935 . 2  |-  ( ( ps  \/  ch  \/  ph )  <->  ( ( ps  \/  ch )  \/ 
ph ) )
41, 2, 33bitr4i 268 1  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ps  \/  ch  \/  ph ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    \/ wo 357    \/ w3o 933
This theorem is referenced by:  3mix2  1125  3mix3  1126  eueq3  2953  tprot  3735  wemapso2lem  7281  ssxr  8908  elnnz  10050  elznn  10055  eliccioo  23131  3orel2  24077  dfon2lem5  24213  dfon2lem6  24214  colinearperm3  24757  dvreasin  25025
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