Theorem 3orrot 1089

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

Syntax hints:   ↔ wb 209   ∨ wo 844   ∨ w3o 1083

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 210  df-or 845  df-3or 1085

This theorem is referenced by:  3orcomb  1091  3mix2  1328  3mix3  1329  eueq3  3650  tprot  4645  wemapsolem  8998  ssxr  10699  elnnz  11979  elznn  11985  pfxnd0  14041  colrot1  26353  lnrot1  26417  lnrot2  26418  3orel2  33054  dfon2lem5  33145  dfon2lem6  33146  nolt02o  33312  nosupbnd2lem1  33328  colinearperm3  33637  wl-exeq  34939  dvasin  35141  frege129d  40464