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