Metamath Proof Explorer

Theorem or42

Description: Rearrangement of 4 disjuncts. (Contributed by NM, 10-Jan-2005)

Ref Expression
Assertion or42 ⊢ φ ∨ ψ ∨ χ ∨ θ ↔ φ ∨ χ ∨ θ ∨ ψ

Proof

Step Hyp Ref Expression
1 or4 ⊢ φ ∨ ψ ∨ χ ∨ θ ↔ φ ∨ χ ∨ ψ ∨ θ
2 orcom ⊢ ψ ∨ θ ↔ θ ∨ ψ
3 2 orbi2i ⊢ φ ∨ χ ∨ ψ ∨ θ ↔ φ ∨ χ ∨ θ ∨ ψ
4 1 3 bitri ⊢ φ ∨ ψ ∨ χ ∨ θ ↔ φ ∨ χ ∨ θ ∨ ψ