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

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

Proof of Theorem 3orrot
StepHypRef Expression
1 orcom 870 . 2 ((𝜑 ∨ (𝜓𝜒)) ↔ ((𝜓𝜒) ∨ 𝜑))
2 3orass 1089 . 2 ((𝜑𝜓𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
3 df-3or 1087 . 2 ((𝜓𝜒𝜑) ↔ ((𝜓𝜒) ∨ 𝜑))
41, 2, 33bitr4i 303 1 ((𝜑𝜓𝜒) ↔ (𝜓𝜒𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wo 847  w3o 1085
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 207  df-or 848  df-3or 1087
This theorem is referenced by:  3orcomb  1093  3mix2  1330  3mix3  1331  3orel2  1483  eueq3  3719  tprot  4753  wemapsolem  9587  ssxr  11327  elnnz  12620  elznn  12626  pfxnd0  14722  nolt02o  27754  nosupbnd2lem1  27774  colrot1  28581  lnrot1  28645  lnrot2  28646  dfon2lem5  35768  dfon2lem6  35769  colinearperm3  36044  wl-exeq  37514  dvasin  37690  frege129d  43752  usgrexmpl2nb0  47925  usgrexmpl2nb3  47928
  Copyright terms: Public domain W3C validator