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