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