Theorem andir 866

Description: Distributive law for conjunction. (Contributed by NM, 12-Aug-1994.)

Assertion

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

Proof of Theorem andir

Step	Hyp	Ref	Expression
1		andi 865	. 2 |- ( ( ch /\ ( ph \/ ps ) ) <-> ( ( ch /\ ph ) \/ ( ch /\ ps ) ) )
2		ancom 448	. 2 |- ( ( ( ph \/ ps ) /\ ch ) <-> ( ch /\ ( ph \/ ps ) ) )
3		ancom 448	. . 3 |- ( ( ph /\ ch ) <-> ( ch /\ ph ) )
4		ancom 448	. . 3 |- ( ( ps /\ ch ) <-> ( ch /\ ps ) )
5	3, 4	orbi12i 519	. 2 |- ( ( ( ph /\ ch ) \/ ( ps /\ ch ) ) <-> ( ( ch /\ ph ) \/ ( ch /\ ps ) ) )
6	1, 2, 5	3bitr4i 277	1 |- ( ( ( ph \/ ps ) /\ ch ) <-> ( ( ph /\ ch ) \/ ( ps /\ ch ) ) )

Syntax hints:   <-> wb 184   \/ wo 366   /\ wa 367

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

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369

This theorem is referenced by:  anddi  868  cases  968  cador  1465  rexun  3598  rabun2  3702  reuun2  3706  xpundir  4967  coundi  5416  mptun  5620  tpostpos  6893  wemapsolem  7890  ltxr  11245  hashbclem  12405  hashf1lem2  12409  pythagtriplem2  14343  pythagtrip  14360  vdwapun  14494  legtrid  24098  colinearalg  24334  usgraedg4  24508  vdgrun  25022  vdgrfiun  25023  elimifd  27546  dfon2lem5  29384  nobndup  29625  nofulllem5  29631  seglelin  29919  cnambfre  30228  expdioph  31131  usgvincvad  32722  usgvincvadALT  32725  rp-isfinite6  38173