Theorem 3orrot 1108

Description: Rotation law for triple disjunction. (Contributed by NM, 4-Apr-1995.)

Assertion

Ref	Expression
3orrot	⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑))

Proof of Theorem 3orrot

Step	Hyp	Ref	Expression
1		orcom 883	. 2 ⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) ↔ ((𝜓 ∨ 𝜒) ∨ 𝜑))
2		3orass 1106	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
3		df-3or 1104	. 2 ⊢ ((𝜓 ∨ 𝜒 ∨ 𝜑) ↔ ((𝜓 ∨ 𝜒) ∨ 𝜑))
4	1, 2, 3	3bitr4i 306	1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑))

Syntax hints:   ↔ wb 209   ∨ wo 860   ∨ w3o 1102

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 861  df-3or 1104

This theorem is referenced by:  3orcomb  1110  3mix2  1350  3mix3  1351  3orel2OLD  1516  eueq3  3674  tprot  4715  wemapsolem  9508  ssxr  11274  elnnz  12596  elznn  12602  pfxnd0  14722  nolt02o  27859  nosupbnd2lem1  27879  colrot1  28828  lnrot1  28896  lnrot2  28897  dfon2lem5  36277  dfon2lem6  36278  colinearperm3  36555  wl-exeq  38189  dvasin  38355  frege129d  44489  usgrexmpl2nb0  48796  usgrexmpl2nb3  48799