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 ⊢φ∨ψ∨χ∨θ↔φ∨χ∨θ∨ψ