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

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

Proof of Theorem 3orrot
StepHypRef Expression
1 orcom 866 . 2 ((𝜑 ∨ (𝜓𝜒)) ↔ ((𝜓𝜒) ∨ 𝜑))
2 3orass 1084 . 2 ((𝜑𝜓𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
3 df-3or 1082 . 2 ((𝜓𝜒𝜑) ↔ ((𝜓𝜒) ∨ 𝜑))
41, 2, 33bitr4i 304 1 ((𝜑𝜓𝜒) ↔ (𝜓𝜒𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 207  wo 843  w3o 1080
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 208  df-or 844  df-3or 1082
This theorem is referenced by:  3orcomb  1088  3mix2  1325  3mix3  1326  eueq3  3706  tprot  4684  wemapsolem  9003  ssxr  10699  elnnz  11980  elznn  11986  pfxnd0  14040  colrot1  26262  lnrot1  26326  lnrot2  26327  3orel2  32828  dfon2lem5  32919  dfon2lem6  32920  nolt02o  33086  nosupbnd2lem1  33102  colinearperm3  33411  wl-exeq  34645  dvasin  34848  frege129d  39976
  Copyright terms: Public domain W3C validator