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 303 1 ((𝜑𝜓𝜒) ↔ (𝜓𝜒𝜑))
Colors of variables: wff setvar class
Syntax hints:  wb 205  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 206  df-or 847  df-3or 1089
This theorem is referenced by:  3orcomb  1095  3mix2  1332  3mix3  1333  3orel2  1486  eueq3  3708  tprot  4754  wemapsolem  9545  ssxr  11283  elnnz  12568  elznn  12574  pfxnd0  14638  nolt02o  27198  nosupbnd2lem1  27218  colrot1  27810  lnrot1  27874  lnrot2  27875  dfon2lem5  34759  dfon2lem6  34760  colinearperm3  35035  wl-exeq  36403  dvasin  36572  frege129d  42514
  Copyright terms: Public domain W3C validator