Theorem andi 604

Description: Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell] p. 118.

Assertion

Ref	Expression
andi	|- ((ph /\ (ps \/ ch)) <-> ((ph /\ ps) \/ (ph /\ ch)))

Proof of Theorem andi

Step	Hyp	Ref	Expression
1		ordi 596	. . . 4 |- ((-. ph \/ (-. ps /\ -. ch)) <-> ((-. ph \/ -. ps) /\ (-. ph \/ -. ch)))
2		ioran 306	. . . . 5 |- (-. (ps \/ ch) <-> (-. ps /\ -. ch))
3	2	orbi2i 255	. . . 4 |- ((-. ph \/ -. (ps \/ ch)) <-> (-. ph \/ (-. ps /\ -. ch)))
4		ianor 305	. . . . 5 |- (-. (ph /\ ps) <-> (-. ph \/ -. ps))
5		ianor 305	. . . . 5 |- (-. (ph /\ ch) <-> (-. ph \/ -. ch))
6	4, 5	anbi12i 482	. . . 4 |- ((-. (ph /\ ps) /\ -. (ph /\ ch)) <-> ((-. ph \/ -. ps) /\ (-. ph \/ -. ch)))
7	1, 3, 6	3bitr4 183	. . 3 |- ((-. ph \/ -. (ps \/ ch)) <-> (-. (ph /\ ps) /\ -. (ph /\ ch)))
8	7	negbii 187	. 2 |- (-. (-. ph \/ -. (ps \/ ch)) <-> -. (-. (ph /\ ps) /\ -. (ph /\ ch)))
9		anor 304	. 2 |- ((ph /\ (ps \/ ch)) <-> -. (-. ph \/ -. (ps \/ ch)))
10		oran 312	. 2 |- (((ph /\ ps) \/ (ph /\ ch)) <-> -. (-. (ph /\ ps) /\ -. (ph /\ ch)))
11	8, 9, 10	3bitr4 183	1 |- ((ph /\ (ps \/ ch)) <-> ((ph /\ ps) \/ (ph /\ ch)))

Syntax hints:  -. wn 2   <-> wb 146   \/ wo 222   /\ wa 223

This theorem is referenced by:  andir 605  anddi 607  prlem2 771  r19.43 1765  indi 2251  unrab 2270  unipr 2515  uniun 2519  unopab 2679  ordnbtwn 3063  onzsl 3117  xpundi 3225  imadif 3574  dfrdg2 3933  elznn0nn 6148  elnn0nn 6171  icounlem 6412  snunioolem 6414  ioojoint 6416  faclbnd4lem4 6951  efifolem2 8723

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225

Copyright terms: Public domain