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

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

Proof of Theorem 3orrot
StepHypRef Expression
1 orcom 402 . 2 ((𝜑 ∨ (𝜓𝜒)) ↔ ((𝜓𝜒) ∨ 𝜑))
2 3orass 1039 . 2 ((𝜑𝜓𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
3 df-3or 1037 . 2 ((𝜓𝜒𝜑) ↔ ((𝜓𝜒) ∨ 𝜑))
41, 2, 33bitr4i 292 1 ((𝜑𝜓𝜒) ↔ (𝜓𝜒𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wo 383  w3o 1035
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 197  df-or 385  df-3or 1037
This theorem is referenced by:  3mix2  1229  3mix3  1230  eueq3  3375  tprot  4275  wemapsolem  8440  ssxr  10092  elnnz  11372  elznn  11378  colrot1  25435  lnrot1  25499  lnrot2  25500  3orel2  31567  dfon2lem5  31666  dfon2lem6  31667  nolt02o  31819  nosupbnd2lem1  31835  colinearperm3  32145  wl-exeq  33292  dvasin  33467  frege129d  37874
  Copyright terms: Public domain W3C validator