Theorem 3orrot 1103

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 881	. 2 ⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) ↔ ((𝜓 ∨ 𝜒) ∨ 𝜑))
2		3orass 1101	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
3		df-3or 1099	. 2 ⊢ ((𝜓 ∨ 𝜒 ∨ 𝜑) ↔ ((𝜓 ∨ 𝜒) ∨ 𝜑))
4	1, 2, 3	3bitr4i 305	1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑))

Syntax hints:   ↔ wb 208   ∨ wo 858   ∨ w3o 1097

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 209  df-or 859  df-3or 1099

This theorem is referenced by:  3orcomb  1105  3mix2  1345  3mix3  1346  3orel2OLD  1506  eueq3  3674  tprot  4708  wemapsolem  9498  ssxr  11252  elnnz  12578  elznn  12584  pfxnd0  14702  nolt02o  27756  nosupbnd2lem1  27776  colrot1  28725  lnrot1  28789  lnrot2  28790  dfon2lem5  36132  dfon2lem6  36133  colinearperm3  36410  wl-exeq  38034  dvasin  38200  frege129d  44336  usgrexmpl2nb0  48650  usgrexmpl2nb3  48653