Metamath Proof Explorer

Theorem andir

Description: Distributive law for conjunction. (Contributed by NM, 12-Aug-1994)

Ref Expression
Assertion andir ⊢ φ ∨ ψ ∧ χ ↔ φ ∧ χ ∨ ψ ∧ χ

Proof

Step Hyp Ref Expression
1 andi ⊢ χ ∧ φ ∨ ψ ↔ χ ∧ φ ∨ χ ∧ ψ
2 ancom ⊢ φ ∨ ψ ∧ χ ↔ χ ∧ φ ∨ ψ
3 ancom ⊢ φ ∧ χ ↔ χ ∧ φ
4 ancom ⊢ ψ ∧ χ ↔ χ ∧ ψ
5 3 4 orbi12i ⊢ φ ∧ χ ∨ ψ ∧ χ ↔ χ ∧ φ ∨ χ ∧ ψ
6 1 2 5 3bitr4i ⊢ φ ∨ ψ ∧ χ ↔ φ ∧ χ ∨ ψ ∧ χ