Metamath Proof Explorer

Theorem anandir

Description: Distribution of conjunction over conjunction. (Contributed by NM, 24-Aug-1995)

Ref Expression
Assertion anandir ⊢ φ ∧ ψ ∧ χ ↔ φ ∧ χ ∧ ψ ∧ χ

Proof

Step Hyp Ref Expression
1 anidm ⊢ χ ∧ χ ↔ χ
2 1 anbi2i ⊢ φ ∧ ψ ∧ χ ∧ χ ↔ φ ∧ ψ ∧ χ
3 an4 ⊢ φ ∧ ψ ∧ χ ∧ χ ↔ φ ∧ χ ∧ ψ ∧ χ
4 2 3 bitr3i ⊢ φ ∧ ψ ∧ χ ↔ φ ∧ χ ∧ ψ ∧ χ