Metamath Proof Explorer

Theorem 3anrev

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

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

Proof

Step Hyp Ref Expression
1 3ancoma ⊢ φ ∧ ψ ∧ χ ↔ ψ ∧ φ ∧ χ
2 3anrot ⊢ χ ∧ ψ ∧ φ ↔ ψ ∧ φ ∧ χ
3 1 2 bitr4i ⊢ φ ∧ ψ ∧ χ ↔ χ ∧ ψ ∧ φ