Metamath Proof Explorer

Theorem 3anrot

Description: Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994) (Proof shortened by Wolf Lammen, 9-Jun-2022)

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

Proof

Step Hyp Ref Expression
1 3ancoma ⊢φ∧ψ∧χ↔ψ∧φ∧χ
2 3ancomb ⊢ψ∧φ∧χ↔ψ∧χ∧φ
3 1 2 bitri ⊢φ∧ψ∧χ↔ψ∧χ∧φ