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  2940  tprot  3722  wemapso2lem  7265  ssxr  8892  elnnz  10034  elznn  10039  eliccioo  23115  3orel2  24062  dfon2lem5  24143  dfon2lem6  24144  colinearperm3  24686  dvreasin  24923
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