Metamath Proof Explorer

Theorem 13an22anass

Description: Associative law for four conjunctions with a triple conjunction. (Contributed by Thierry Arnoux, 21-Jan-2025) (Proof shortened by Wolf Lammen, 31-Oct-2026)

Ref Expression
Assertion 13an22anass ⊢ φ ∧ ψ ∧ χ ∧ θ ↔ φ ∧ ψ ∧ χ ∧ θ

Proof

Step Hyp Ref Expression
1 3anass ⊢ ψ ∧ χ ∧ θ ↔ ψ ∧ χ ∧ θ
2 1 bianass ⊢ φ ∧ ψ ∧ χ ∧ θ ↔ φ ∧ ψ ∧ χ ∧ θ