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

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

Proof of Theorem 3orrot
StepHypRef Expression
1 orcom 401 . 2 ((𝜑 ∨ (𝜓𝜒)) ↔ ((𝜓𝜒) ∨ 𝜑))
2 3orass 1034 . 2 ((𝜑𝜓𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
3 df-3or 1032 . 2 ((𝜓𝜒𝜑) ↔ ((𝜓𝜒) ∨ 𝜑))
41, 2, 33bitr4i 291 1 ((𝜑𝜓𝜒) ↔ (𝜓𝜒𝜑))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∨ wo 382   ∨ w3o 1030 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 196  df-or 384  df-3or 1032 This theorem is referenced by:  3mix2  1224  3mix3  1225  eueq3  3348  tprot  4228  wemapsolem  8338  ssxr  9986  elnnz  11264  elznn  11270  colrot1  25254  lnrot1  25318  lnrot2  25319  3orel2  30847  dfon2lem5  30936  dfon2lem6  30937  colinearperm3  31340  wl-exeq  32500  dvasin  32666  frege129d  37074
 Copyright terms: Public domain W3C validator