Metamath Proof Explorer

Theorem or4

Description: Rearrangement of 4 disjuncts. (Contributed by NM, 12-Aug-1994)

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

Proof

Step Hyp Ref Expression
1 or12 ⊢ψ∨χ∨θ↔χ∨ψ∨θ
2 1 orbi2i ⊢φ∨ψ∨χ∨θ↔φ∨χ∨ψ∨θ
3 orass ⊢φ∨ψ∨χ∨θ↔φ∨ψ∨χ∨θ
4 orass ⊢φ∨χ∨ψ∨θ↔φ∨χ∨ψ∨θ
5 2 3 4 3bitr4i ⊢φ∨ψ∨χ∨θ↔φ∨χ∨ψ∨θ