Theorem 3orrot 1091

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

Syntax hints:   ↔ wb 206   ∨ wo 847   ∨ w3o 1085

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 207  df-or 848  df-3or 1087

This theorem is referenced by:  3orcomb  1093  3mix2  1332  3mix3  1333  3orel2OLD  1487  eueq3  3665  tprot  4699  wemapsolem  9436  ssxr  11182  elnnz  12478  elznn  12484  pfxnd0  14596  nolt02o  27634  nosupbnd2lem1  27654  colrot1  28537  lnrot1  28601  lnrot2  28602  dfon2lem5  35829  dfon2lem6  35830  colinearperm3  36105  wl-exeq  37576  dvasin  37752  frege129d  43804  usgrexmpl2nb0  48070  usgrexmpl2nb3  48073