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

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

Proof of Theorem 3orrot
StepHypRef Expression
1 orcom 871 . 2 ((𝜑 ∨ (𝜓𝜒)) ↔ ((𝜓𝜒) ∨ 𝜑))
2 3orass 1090 . 2 ((𝜑𝜓𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
3 df-3or 1088 . 2 ((𝜓𝜒𝜑) ↔ ((𝜓𝜒) ∨ 𝜑))
41, 2, 33bitr4i 303 1 ((𝜑𝜓𝜒) ↔ (𝜓𝜒𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wo 848  w3o 1086
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 849  df-3or 1088
This theorem is referenced by:  3orcomb  1094  3mix2  1332  3mix3  1333  3orel2OLD  1487  eueq3  3717  tprot  4749  wemapsolem  9590  ssxr  11330  elnnz  12623  elznn  12629  pfxnd0  14726  nolt02o  27740  nosupbnd2lem1  27760  colrot1  28567  lnrot1  28631  lnrot2  28632  dfon2lem5  35788  dfon2lem6  35789  colinearperm3  36064  wl-exeq  37535  dvasin  37711  frege129d  43776  usgrexmpl2nb0  47990  usgrexmpl2nb3  47993
  Copyright terms: Public domain W3C validator