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

Theorem 3orrot 1061
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 1057 . 2 ((𝜑𝜓𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
3 df-3or 1055 . 2 ((𝜓𝜒𝜑) ↔ ((𝜓𝜒) ∨ 𝜑))
41, 2, 33bitr4i 292 1 ((𝜑𝜓𝜒) ↔ (𝜓𝜒𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wo 382  w3o 1053
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 384  df-3or 1055
This theorem is referenced by:  3orcomb  1065  3mix2  1251  3mix3  1252  eueq3  3414  tprot  4316  wemapsolem  8496  ssxr  10145  elnnz  11425  elznn  11431  colrot1  25499  lnrot1  25563  lnrot2  25564  3orel2  31718  dfon2lem5  31816  dfon2lem6  31817  nolt02o  31970  nosupbnd2lem1  31986  colinearperm3  32295  wl-exeq  33451  dvasin  33626  frege129d  38372
  Copyright terms: Public domain W3C validator