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 φ ψ χ φ χ ψ χ