Theorem andir 912

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 911	. 2 |- ( ( ch /\ ( ph \/ ps ) ) <-> ( ( ch /\ ph ) \/ ( ch /\ ps ) ) )
2		ancom 466	. 2 |- ( ( ( ph \/ ps ) /\ ch ) <-> ( ch /\ ( ph \/ ps ) ) )
3		ancom 466	. . 3 |- ( ( ph /\ ch ) <-> ( ch /\ ph ) )
4		ancom 466	. . 3 |- ( ( ps /\ ch ) <-> ( ch /\ ps ) )
5	3, 4	orbi12i 543	. 2 |- ( ( ( ph /\ ch ) \/ ( ps /\ ch ) ) <-> ( ( ch /\ ph ) \/ ( ch /\ ps ) ) )
6	1, 2, 5	3bitr4i 292	1 |- ( ( ( ph \/ ps ) /\ ch ) <-> ( ( ph /\ ch ) \/ ( ps /\ ch ) ) )

Syntax hints:   <-> wb 196   \/ wo 383   /\ wa 384

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 197  df-or 385  df-an 386

This theorem is referenced by:  anddi  914  cases  992  cador  1547  rexun  3793  rabun2  3906  reuun2  3910  xpundir  5172  coundi  5636  mptun  6025  tpostpos  7372  wemapsolem  8455  ltxr  11949  hashbclem  13236  hashf1lem2  13240  pythagtriplem2  15522  pythagtrip  15539  vdwapun  15678  legtrid  25486  colinearalg  25790  vtxdun  26377  elimifd  29362  dfon2lem5  31692  seglelin  32223  poimirlem30  33439  poimirlem31  33440  cnambfre  33458  expdioph  37590  rp-isfinite6  37864  uneqsn  38321