Theorem andi 826

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 720	. . 3 |- ( ( ph /\ ps ) -> ( ( ph /\ ps ) \/ ( ph /\ ch ) ) )
2		olc 719	. . 3 |- ( ( ph /\ ch ) -> ( ( ph /\ ps ) \/ ( ph /\ ch ) ) )
3	1, 2	jaodan 805	. 2 |- ( ( ph /\ ( ps \/ ch ) ) -> ( ( ph /\ ps ) \/ ( ph /\ ch ) ) )
4		orc 720	. . . 4 |- ( ps -> ( ps \/ ch ) )
5	4	anim2i 342	. . 3 |- ( ( ph /\ ps ) -> ( ph /\ ( ps \/ ch ) ) )
6		olc 719	. . . 4 |- ( ch -> ( ps \/ ch ) )
7	6	anim2i 342	. . 3 |- ( ( ph /\ ch ) -> ( ph /\ ( ps \/ ch ) ) )
8	5, 7	jaoi 724	. 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 716

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  andir  827  anddi  829  dcim  849  excxor  1423  sbequilem  1887  sborv  1940  r19.43  2701  indi  3468  difindiss  3475  unrab  3492  unipr  3928  uniun  3933  unopab  4189  xpundi  4806  coundir  5265  unpreima  5802  tpostpos  6495  elni2  7629  elznn0nn  9591  lgsquadlem3  15952