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

Theorem 3orrot 942
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 377 . 2  |-  ( (
ph  \/  ( ps  \/  ch ) )  <->  ( ( ps  \/  ch )  \/ 
ph ) )
2 3orass 939 . 2  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ph  \/  ( ps  \/  ch ) ) )
3 df-3or 937 . 2  |-  ( ( ps  \/  ch  \/  ph )  <->  ( ( ps  \/  ch )  \/ 
ph ) )
41, 2, 33bitr4i 269 1  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ps  \/  ch  \/  ph ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    \/ wo 358    \/ w3o 935
This theorem is referenced by:  3mix2  1127  3mix3  1128  eueq3  3069  tprot  3859  wemapso2lem  7475  ssxr  9101  elnnz  10248  elznn  10253  3orel2  25118  dfon2lem5  25357  dfon2lem6  25358  colinearperm3  25901  dvreasin  26179
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 178  df-or 360  df-3or 937
  Copyright terms: Public domain W3C validator