Theorem 3orcomb 1110

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 1109	. 2 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜓 ∨ 𝜑 ∨ 𝜒))
2		3orrot 1108	. 2 ⊢ ((𝜓 ∨ 𝜑 ∨ 𝜒) ↔ (𝜑 ∨ 𝜒 ∨ 𝜓))
3	1, 2	bitri 278	1 ⊢ ((𝜑 ∨ 𝜓 ∨ 𝜒) ↔ (𝜑 ∨ 𝜒 ∨ 𝜓))

This proof depends on syntax axioms:   ↔ wb 209   ∨ w3o 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862  df-3or 1104

This theorem is used by:  eueq3  3669  oneltri  6403  soseq  8162  swoso  8738  swrdnd  14749  elnnzs  28698  colcom  28932  legso  28973  lncom  29001  vonf1wev  35788  vonf1owevOLD  35790  colinearperm1  36725  frege129d  44668  ordelordALT  45425  ordelordALTVD  45754  chnerlem3  47777  usgrexmpl2nb3  49015