Theorem andir 884

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 883	. 2 |- ( ( ch /\ ( ph \/ ps ) ) <-> ( ( ch /\ ph ) \/ ( ch /\ ps ) ) )
2		ancom 456	. 2 |- ( ( ( ph \/ ps ) /\ ch ) <-> ( ch /\ ( ph \/ ps ) ) )
3		ancom 456	. . 3 |- ( ( ph /\ ch ) <-> ( ch /\ ph ) )
4		ancom 456	. . 3 |- ( ( ps /\ ch ) <-> ( ch /\ ps ) )
5	3, 4	orbi12i 528	. 2 |- ( ( ( ph /\ ch ) \/ ( ps /\ ch ) ) <-> ( ( ch /\ ph ) \/ ( ch /\ ps ) ) )
6	1, 2, 5	3bitr4i 285	1 |- ( ( ( ph \/ ps ) /\ ch ) <-> ( ( ph /\ ch ) \/ ( ps /\ ch ) ) )

Syntax hints:   <-> wb 189   \/ wo 374   /\ wa 375

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 190  df-or 376  df-an 377

This theorem is referenced by:  anddi  886  cases  988  cador  1522  rexun  3626  rabun2  3734  reuun2  3738  xpundir  4907  coundi  5355  mptun  5731  tpostpos  7019  wemapsolem  8091  ltxr  11444  hashbclem  12648  hashf1lem2  12652  pythagtriplem2  14816  pythagtrip  14833  vdwapun  14973  legtrid  24685  colinearalg  24989  usgraedg4  25163  vdgrun  25678  vdgrfiun  25679  elimifd  28209  dfon2lem5  30482  nobndup  30638  nofulllem5  30644  seglelin  30932  poimirlem30  32015  poimirlem31  32016  cnambfre  32034  expdioph  35923  rp-isfinite6  36208  vtxduhgrun  39588  usgvincvad  39989  usgvincvadALT  39992