Metamath Proof Explorer

Theorem anandi

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

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

Proof

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