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	|- ( ( ph /\ ( ps \/ ch ) ) <-> ( ( ph /\ ps ) \/ ( ph /\ ch ) ) )

Proof

Step	Hyp	Ref	Expression
1		orc	|- ( ( ph /\ ps ) -> ( ( ph /\ ps ) \/ ( ph /\ ch ) ) )
2		olc	|- ( ( ph /\ ch ) -> ( ( ph /\ ps ) \/ ( ph /\ ch ) ) )
3	1 2	jaodan	|- ( ( ph /\ ( ps \/ ch ) ) -> ( ( ph /\ ps ) \/ ( ph /\ ch ) ) )
4		orc	|- ( ps -> ( ps \/ ch ) )
5	4	anim2i	|- ( ( ph /\ ps ) -> ( ph /\ ( ps \/ ch ) ) )
6		olc	|- ( ch -> ( ps \/ ch ) )
7	6	anim2i	|- ( ( ph /\ ch ) -> ( ph /\ ( ps \/ ch ) ) )
8	5 7	jaoi	|- ( ( ( ph /\ ps ) \/ ( ph /\ ch ) ) -> ( ph /\ ( ps \/ ch ) ) )
9	3 8	impbii	|- ( ( ph /\ ( ps \/ ch ) ) <-> ( ( ph /\ ps ) \/ ( ph /\ ch ) ) )