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 ⊢φ∧ψ∧χ↔φ∧χ∧ψ∧χ