Theorem 3orrot 1106

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 1104	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
3		df-3or 1102	. 2 ⊢ ((𝜓 ∨ 𝜒 ∨ 𝜑) ↔ ((𝜓 ∨ 𝜒) ∨ 𝜑))
4	1, 2, 3	3bitr4i 306	1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑))

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

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 1102

This theorem is referenced by:  3orcomb  1108  3mix2  1348  3mix3  1349  3orel2OLD  1513  eueq3  3683  tprot  4720  wemapsolem  9511  ssxr  11278  elnnz  12600  elznn  12606  pfxnd0  14725  nolt02o  27824  nosupbnd2lem1  27844  colrot1  28793  lnrot1  28857  lnrot2  28858  dfon2lem5  36175  dfon2lem6  36176  colinearperm3  36453  wl-exeq  38076  dvasin  38242  frege129d  44380  usgrexmpl2nb0  48684  usgrexmpl2nb3  48687