Theorem andi 607

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 599	. . . 4 |- ((-. ph \/ (-. ps /\ -. ch)) <-> ((-. ph \/ -. ps) /\ (-. ph \/ -. ch)))
2		ioran 304	. . . . 5 |- (-. (ps \/ ch) <-> (-. ps /\ -. ch))
3	2	orbi2i 253	. . . 4 |- ((-. ph \/ -. (ps \/ ch)) <-> (-. ph \/ (-. ps /\ -. ch)))
4		ianor 303	. . . . 5 |- (-. (ph /\ ps) <-> (-. ph \/ -. ps))
5		ianor 303	. . . . 5 |- (-. (ph /\ ch) <-> (-. ph \/ -. ch))
6	4, 5	anbi12i 485	. . . 4 |- ((-. (ph /\ ps) /\ -. (ph /\ ch)) <-> ((-. ph \/ -. ps) /\ (-. ph \/ -. ch)))
7	1, 3, 6	3bitr4i 181	. . 3 |- ((-. ph \/ -. (ps \/ ch)) <-> (-. (ph /\ ps) /\ -. (ph /\ ch)))
8	7	notbii 185	. 2 |- (-. (-. ph \/ -. (ps \/ ch)) <-> -. (-. (ph /\ ps) /\ -. (ph /\ ch)))
9		anor 302	. 2 |- ((ph /\ (ps \/ ch)) <-> -. (-. ph \/ -. (ps \/ ch)))
10		oran 310	. 2 |- (((ph /\ ps) \/ (ph /\ ch)) <-> -. (-. (ph /\ ps) /\ -. (ph /\ ch)))
11	8, 9, 10	3bitr4i 181	1 |- ((ph /\ (ps \/ ch)) <-> ((ph /\ ps) \/ (ph /\ ch)))

Syntax hints:  -. wn 2   <-> wb 144   \/ wo 220   /\ wa 221

This theorem is referenced by:  andir 608  anddi 610  prlem2 776  r19.43 1811  indi 2303  unrab 2322  unipr 2581  uniun 2586  unopab 2753  ordnbtwn 3062  onzsl 3200  xpundi 3310  coundir 3601  imadif 3679  dfrdg2 4234  elznn0nn 6316  elnn0nn 6339  icounlem 6539  snunioolem 6541  ioojoin 6543  fzsuc 6636  faclbnd4lem4 7154  efifolem2 8995  anddi2 10718  unpreima 11794

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 145  df-or 222  df-an 223

Copyright terms: Public domain