Theorem 3orrot 1093

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 869	. 2 ⊢ ((𝜑 ∨ (𝜓 ∨ 𝜒)) ↔ ((𝜓 ∨ 𝜒) ∨ 𝜑))
2		3orass 1091	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ (𝜓 ∨ 𝜒)))
3		df-3or 1089	. 2 ⊢ ((𝜓 ∨ 𝜒 ∨ 𝜑) ↔ ((𝜓 ∨ 𝜒) ∨ 𝜑))
4	1, 2, 3	3bitr4i 303	1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒 ∨ 𝜑))

Syntax hints:   ↔ wb 205   ∨ wo 846   ∨ w3o 1087

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 206  df-or 847  df-3or 1089

This theorem is referenced by:  3orcomb  1095  3mix2  1332  3mix3  1333  3orel2  1486  eueq3  3708  tprot  4754  wemapsolem  9545  ssxr  11283  elnnz  12568  elznn  12574  pfxnd0  14638  nolt02o  27198  nosupbnd2lem1  27218  colrot1  27841  lnrot1  27905  lnrot2  27906  dfon2lem5  34790  dfon2lem6  34791  colinearperm3  35066  wl-exeq  36451  dvasin  36620  frege129d  42562