Theorem andi 830

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

Assertion

Ref	Expression
andi	|- ( ( ph /\ ( ps \/ ch ) ) <-> ( ( ph /\ ps ) \/ ( ph /\ ch ) ) )

Proof of Theorem andi

Step	Hyp	Ref	Expression
1		orc 724	. . 3 |- ( ( ph /\ ps ) -> ( ( ph /\ ps ) \/ ( ph /\ ch ) ) )
2		olc 723	. . 3 |- ( ( ph /\ ch ) -> ( ( ph /\ ps ) \/ ( ph /\ ch ) ) )
3	1, 2	jaodan 809	. 2 |- ( ( ph /\ ( ps \/ ch ) ) -> ( ( ph /\ ps ) \/ ( ph /\ ch ) ) )
4		orc 724	. . . 4 |- ( ps -> ( ps \/ ch ) )
5	4	anim2i 342	. . 3 |- ( ( ph /\ ps ) -> ( ph /\ ( ps \/ ch ) ) )
6		olc 723	. . . 4 |- ( ch -> ( ps \/ ch ) )
7	6	anim2i 342	. . 3 |- ( ( ph /\ ch ) -> ( ph /\ ( ps \/ ch ) ) )
8	5, 7	jaoi 728	. 2 |- ( ( ( ph /\ ps ) \/ ( ph /\ ch ) ) -> ( ph /\ ( ps \/ ch ) ) )
9	3, 8	impbii 126	1 |- ( ( ph /\ ( ps \/ ch ) ) <-> ( ( ph /\ ps ) \/ ( ph /\ ch ) ) )

This proof depends on syntax axioms:   /\ wa 104   <-> wb 105   \/ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  andir  831  anddi  833  dcim  853  excxor  1427  sbequilem  1891  sborv  1945  r19.43  2709  indi  3478  difindiss  3485  unrab  3504  unipr  3949  uniun  3954  unopab  4210  xpundi  4831  coundir  5290  unpreima  5833  tpostpos  6535  elni2  7681  elznn0nn  9658  lgsquadlem3  16198