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

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

Proof of Theorem 3orrot
StepHypRef Expression
1 orcom 869 . 2 ((𝜑 ∨ (𝜓𝜒)) ↔ ((𝜓𝜒) ∨ 𝜑))
2 3orass 1091 . 2 ((𝜑𝜓𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
3 df-3or 1089 . 2 ((𝜓𝜒𝜑) ↔ ((𝜓𝜒) ∨ 𝜑))
41, 2, 33bitr4i 306 1 ((𝜑𝜓𝜒) ↔ (𝜓𝜒𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wo 846  w3o 1087
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 210  df-or 847  df-3or 1089
This theorem is referenced by:  3orcomb  1095  3mix2  1332  3mix3  1333  eueq3  3610  tprot  4640  wemapsolem  9087  ssxr  10788  elnnz  12072  elznn  12078  pfxnd0  14139  colrot1  26505  lnrot1  26569  lnrot2  26570  3orel2  33227  dfon2lem5  33335  dfon2lem6  33336  nolt02o  33539  nosupbnd2lem1  33559  colinearperm3  34003  wl-exeq  35316  dvasin  35484  frege129d  40917
  Copyright terms: Public domain W3C validator