Metamath Proof Explorer


Theorem andi

Description: Distributive law for conjunction. Theorem *4.4 of WhiteheadRussell p. 118. (Contributed by NM, 21-Jun-1993) (Proof shortened by Wolf Lammen, 5-Jan-2013)

Ref Expression
Assertion andi φ ψ χ φ ψ φ χ

Proof

Step Hyp Ref Expression
1 orc φ ψ φ ψ φ χ
2 olc φ χ φ ψ φ χ
3 1 2 jaodan φ ψ χ φ ψ φ χ
4 orc ψ ψ χ
5 4 anim2i φ ψ φ ψ χ
6 olc χ ψ χ
7 6 anim2i φ χ φ ψ χ
8 5 7 jaoi φ ψ φ χ φ ψ χ
9 3 8 impbii φ ψ χ φ ψ φ χ