Theorem andi 808

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 702	. . 3 |- ( ( ph /\ ps ) -> ( ( ph /\ ps ) \/ ( ph /\ ch ) ) )
2		olc 701	. . 3 |- ( ( ph /\ ch ) -> ( ( ph /\ ps ) \/ ( ph /\ ch ) ) )
3	1, 2	jaodan 787	. 2 |- ( ( ph /\ ( ps \/ ch ) ) -> ( ( ph /\ ps ) \/ ( ph /\ ch ) ) )
4		orc 702	. . . 4 |- ( ps -> ( ps \/ ch ) )
5	4	anim2i 340	. . 3 |- ( ( ph /\ ps ) -> ( ph /\ ( ps \/ ch ) ) )
6		olc 701	. . . 4 |- ( ch -> ( ps \/ ch ) )
7	6	anim2i 340	. . 3 |- ( ( ph /\ ch ) -> ( ph /\ ( ps \/ ch ) ) )
8	5, 7	jaoi 706	. 2 |- ( ( ( ph /\ ps ) \/ ( ph /\ ch ) ) -> ( ph /\ ( ps \/ ch ) ) )
9	3, 8	impbii 125	1 |- ( ( ph /\ ( ps \/ ch ) ) <-> ( ( ph /\ ps ) \/ ( ph /\ ch ) ) )

Syntax hints:   /\ wa 103   <-> wb 104   \/ wo 698

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  andir  809  anddi  811  dcim  831  dcan  923  excxor  1368  sbequilem  1826  sborv  1878  r19.43  2624  indi  3369  difindiss  3376  unrab  3393  unipr  3803  uniun  3808  unopab  4061  xpundi  4660  coundir  5106  unpreima  5610  tpostpos  6232  elni2  7255  elznn0nn  9205