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