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

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

Proof of Theorem 3orrot
StepHypRef Expression
1 orcom 896 . 2 ((𝜑 ∨ (𝜓𝜒)) ↔ ((𝜓𝜒) ∨ 𝜑))
2 3orass 1110 . 2 ((𝜑𝜓𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
3 df-3or 1108 . 2 ((𝜓𝜒𝜑) ↔ ((𝜓𝜒) ∨ 𝜑))
41, 2, 33bitr4i 294 1 ((𝜑𝜓𝜒) ↔ (𝜓𝜒𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wo 873  w3o 1106
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 198  df-or 874  df-3or 1108
This theorem is referenced by:  3orcomb  1114  3mix2  1430  3mix3  1431  eueq3  3542  tprot  4441  wemapsolem  8666  ssxr  10365  elnnz  11638  elznn  11644  pfxnd0  13689  colrot1  25759  lnrot1  25823  lnrot2  25824  3orel2  32059  dfon2lem5  32156  dfon2lem6  32157  nolt02o  32310  nosupbnd2lem1  32326  colinearperm3  32635  wl-exeq  33767  dvasin  33940  frege129d  38754
  Copyright terms: Public domain W3C validator