Theorem andi 823

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 717	. . 3 |- ( ( ph /\ ps ) -> ( ( ph /\ ps ) \/ ( ph /\ ch ) ) )
2		olc 716	. . 3 |- ( ( ph /\ ch ) -> ( ( ph /\ ps ) \/ ( ph /\ ch ) ) )
3	1, 2	jaodan 802	. 2 |- ( ( ph /\ ( ps \/ ch ) ) -> ( ( ph /\ ps ) \/ ( ph /\ ch ) ) )
4		orc 717	. . . 4 |- ( ps -> ( ps \/ ch ) )
5	4	anim2i 342	. . 3 |- ( ( ph /\ ps ) -> ( ph /\ ( ps \/ ch ) ) )
6		olc 716	. . . 4 |- ( ch -> ( ps \/ ch ) )
7	6	anim2i 342	. . 3 |- ( ( ph /\ ch ) -> ( ph /\ ( ps \/ ch ) ) )
8	5, 7	jaoi 721	. 2 |- ( ( ( ph /\ ps ) \/ ( ph /\ ch ) ) -> ( ph /\ ( ps \/ ch ) ) )
9	3, 8	impbii 126	1 |- ( ( ph /\ ( ps \/ ch ) ) <-> ( ( ph /\ ps ) \/ ( ph /\ ch ) ) )

Syntax hints:   /\ wa 104   <-> wb 105   \/ wo 713

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  andir  824  anddi  826  dcim  846  excxor  1420  sbequilem  1884  sborv  1937  r19.43  2689  indi  3452  difindiss  3459  unrab  3476  unipr  3905  uniun  3910  unopab  4166  xpundi  4780  coundir  5237  unpreima  5768  tpostpos  6425  elni2  7524  elznn0nn  9483  lgsquadlem3  15798