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

Theorem 3orrot 988
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 388 . 2  |-  ( (
ph  \/  ( ps  \/  ch ) )  <->  ( ( ps  \/  ch )  \/ 
ph ) )
2 3orass 985 . 2  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ph  \/  ( ps  \/  ch ) ) )
3 df-3or 983 . 2  |-  ( ( ps  \/  ch  \/  ph )  <->  ( ( ps  \/  ch )  \/ 
ph ) )
41, 2, 33bitr4i 280 1  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ps  \/  ch  \/  ph ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    \/ wo 369    \/ w3o 981
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 188  df-or 371  df-3or 983
This theorem is referenced by:  3mix2  1175  3mix3  1176  eueq3  3246  tprot  4092  wemapsolem  8067  ssxr  9703  elnnz  10947  elznn  10953  colrot1  24590  lnrot1  24654  lnrot2  24655  3orel2  30338  dfon2lem5  30427  dfon2lem6  30428  colinearperm3  30822  wl-exeq  31780  dvasin  31941  frege129d  36214
  Copyright terms: Public domain W3C validator