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 450	. 2 |- ( ( ( ph \/ ps ) /\ ch ) <-> ( ch /\ ( ph \/ ps ) ) )
3		ancom 450	. . 3 |- ( ( ph /\ ch ) <-> ( ch /\ ph ) )
4		ancom 450	. . 3 |- ( ( ps /\ ch ) <-> ( ch /\ ps ) )
5	3, 4	orbi12i 521	. 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 368   /\ wa 369

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 370  df-an 371

This theorem is referenced by:  anddi  868  jaoi2OLD  967  cases  969  cador  1442  rexun  3684  rabun2  3777  reuun2  3781  xpundir  5052  coundi  5507  mptun  5711  tpostpos  6975  wemapsolem  7974  ltxr  11323  hashbclem  12466  hashf1lem2  12470  pythagtriplem2  14199  pythagtrip  14216  vdwapun  14350  legtrid  23721  colinearalg  23905  usgraedg4  24079  vdgrun  24593  vdgrfiun  24594  elimifd  27111  elim2if  27112  dfon2lem5  28812  nobndup  29053  nofulllem5  29059  seglelin  29359  cnambfre  29656  expdioph  30585  usgvincvad  31887  usgvincvadALT  31890