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

Theorem 3orrot 979
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 387 . 2  |-  ( (
ph  \/  ( ps  \/  ch ) )  <->  ( ( ps  \/  ch )  \/ 
ph ) )
2 3orass 976 . 2  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ph  \/  ( ps  \/  ch ) ) )
3 df-3or 974 . 2  |-  ( ( ps  \/  ch  \/  ph )  <->  ( ( ps  \/  ch )  \/ 
ph ) )
41, 2, 33bitr4i 277 1  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ps  \/  ch  \/  ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    \/ wo 368    \/ w3o 972
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 974
This theorem is referenced by:  3mix2  1166  3mix3  1167  eueq3  3283  tprot  4128  wemapsolem  7987  ssxr  9666  elnnz  10886  elznn  10892  colrot1  23812  lnrot1  23856  lnrot2  23857  3orel2  28913  dfon2lem5  29146  dfon2lem6  29147  colinearperm3  29640  wl-exeq  29914  dvasin  30030
  Copyright terms: Public domain W3C validator