Theorem 3orrot 1097

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 876	. 2 ⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) ↔ ((𝜓 ∨ 𝜒) ∨ 𝜑))
2		3orass 1095	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
3		df-3or 1093	. 2 ⊢ ((𝜓 ∨ 𝜒 ∨ 𝜑) ↔ ((𝜓 ∨ 𝜒) ∨ 𝜑))
4	1, 2, 3	3bitr4i 304	1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑))

Syntax hints:   ↔ wb 207   ∨ wo 853   ∨ w3o 1091

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 208  df-or 854  df-3or 1093

This theorem is referenced by:  3orcomb  1099  3mix2  1338  3mix3  1339  3orel2OLD  1493  eueq3  3652  tprot  4681  wemapsolem  9455  ssxr  11206  elnnz  12525  elznn  12531  pfxnd0  14642  nolt02o  27677  nosupbnd2lem1  27697  colrot1  28645  lnrot1  28709  lnrot2  28710  dfon2lem5  36013  dfon2lem6  36014  colinearperm3  36291  wl-exeq  37905  dvasin  38071  frege129d  44207  usgrexmpl2nb0  48522  usgrexmpl2nb3  48525