Theorem 3orcomb 1094

Description: Commutation law for triple disjunction. (Contributed by Scott Fenton, 20-Apr-2011.) (Proof shortened by Wolf Lammen, 8-Apr-2022.)

Assertion

Ref	Expression
3orcomb	⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ 𝜒 ∨ 𝜓))

Proof of Theorem 3orcomb

Step	Hyp	Ref	Expression
1		3orcoma 1093	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜑 ∨ 𝜒))
2		3orrot 1092	. 2 ⊢ ((𝜓 ∨ 𝜑 ∨ 𝜒) ↔ (𝜑 ∨ 𝜒 ∨ 𝜓))
3	1, 2	bitri 275	1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ 𝜒 ∨ 𝜓))

Syntax hints:   ↔ wb 206   ∨ w3o 1086

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 849  df-3or 1088

This theorem is referenced by:  eueq3  3657  oneltri  6366  soseq  8109  swoso  8678  swrdnd  14617  elnnzs  28393  colcom  28626  legso  28667  lncom  28690  vonf1owev  35290  colinearperm1  36244  frege129d  44190  ordelordALT  44964  ordelordALTVD  45293  chnerlem3  47314  usgrexmpl2nb3  48510