Theorem andi 730

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 632	. . 3 |- ((ph /\ ps) -> ((ph /\ ps) \/ (ph /\ ch)))
2		olc 631	. . 3 |- ((ph /\ ch) -> ((ph /\ ps) \/ (ph /\ ch)))
3	1, 2	jaodan 709	. 2 |- ((ph /\ (ps \/ ch)) -> ((ph /\ ps) \/ (ph /\ ch)))
4		orc 632	. . . 4 |- (ps -> (ps \/ ch))
5	4	anim2i 324	. . 3 |- ((ph /\ ps) -> (ph /\ (ps \/ ch)))
6		olc 631	. . . 4 |- (ch -> (ps \/ ch))
7	6	anim2i 324	. . 3 |- ((ph /\ ch) -> (ph /\ (ps \/ ch)))
8	5, 7	jaoi 635	. 2 |- (((ph /\ ps) \/ (ph /\ ch)) -> (ph /\ (ps \/ ch)))
9	3, 8	impbii 117	1 |- ((ph /\ (ps \/ ch)) <-> ((ph /\ ps) \/ (ph /\ ch)))

Syntax hints:   /\ wa 97   <-> wb 98   \/ wo 628

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  andir  731  anddi  733  dcim  783  dcan  841  excxor  1268  sbequilem  1716  sborv  1767  r19.43  2462  indi  3178  difindiss  3185  unrab  3202  unipr  3585  uniun  3590  unopab  3827  xpundi  4339  coundir  4766  unpreima  5235  tpostpos  5820  elni2  6298  elznn0nn  8035