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