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 φ ψ χ φ ψ χ