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

Theorem 3orrot 979
Description: Rotation law for triple disjunction. (Contributed by NM, 4-Apr-1995.)
Assertion
Ref Expression
3orrot

Proof of Theorem 3orrot
StepHypRef Expression
1 orcom 387 . 2
2 3orass 976 . 2
3 df-3or 974 . 2
41, 2, 33bitr4i 277 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  \/wo 368  \/w3o 972
This theorem is referenced by:  3mix2  1166  3mix3  1167  eueq3  3274  tprot  4125  wemapsolem  7996  ssxr  9675  elnnz  10899  elznn  10905  colrot1  23946  lnrot1  24003  lnrot2  24004  3orel2  29088  dfon2lem5  29219  dfon2lem6  29220  colinearperm3  29713  wl-exeq  29987  dvasin  30103
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
  Copyright terms: Public domain W3C validator