Metamath Proof Explorer

Theorem anandi3

Description: Distribution of triple conjunction over conjunction. (Contributed by David A. Wheeler, 4-Nov-2018)

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

Proof

Step Hyp Ref Expression
1 3anass ⊢ φ ∧ ψ ∧ χ ↔ φ ∧ ψ ∧ χ
2 anandi ⊢ φ ∧ ψ ∧ χ ↔ φ ∧ ψ ∧ φ ∧ χ
3 1 2 bitri ⊢ φ ∧ ψ ∧ χ ↔ φ ∧ ψ ∧ φ ∧ χ