Metamath Proof Explorer

Theorem 3anass

Description: Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994)

Ref Expression
Assertion 3anass ⊢ φ ∧ ψ ∧ χ ↔ φ ∧ ψ ∧ χ

Proof

Step Hyp Ref Expression
1 df-3an ⊢ φ ∧ ψ ∧ χ ↔ φ ∧ ψ ∧ χ
2 anass ⊢ φ ∧ ψ ∧ χ ↔ φ ∧ ψ ∧ χ
3 1 2 bitri ⊢ φ ∧ ψ ∧ χ ↔ φ ∧ ψ ∧ χ