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  1941  r19.43  2703  indi  3472  difindiss  3479  unrab  3496  unipr  3933  uniun  3938  unopab  4194  xpundi  4811  coundir  5270  unpreima  5807  tpostpos  6508  elni2  7645  elznn0nn  9608  lgsquadlem3  16078