Theorem 3orrot 1061

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 401	. 2 ⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) ↔ ((𝜓 ∨ 𝜒) ∨ 𝜑))
2		3orass 1057	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
3		df-3or 1055	. 2 ⊢ ((𝜓 ∨ 𝜒 ∨ 𝜑) ↔ ((𝜓 ∨ 𝜒) ∨ 𝜑))
4	1, 2, 3	3bitr4i 292	1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑))

Syntax hints:   ↔ wb 196   ∨ wo 382   ∨ w3o 1053

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 197  df-or 384  df-3or 1055

This theorem is referenced by:  3orcomb  1065  3mix2  1251  3mix3  1252  eueq3  3414  tprot  4316  wemapsolem  8496  ssxr  10145  elnnz  11425  elznn  11431  colrot1  25499  lnrot1  25563  lnrot2  25564  3orel2  31718  dfon2lem5  31816  dfon2lem6  31817  nolt02o  31970  nosupbnd2lem1  31986  colinearperm3  32295  wl-exeq  33451  dvasin  33626  frege129d  38372