Theorem andir 858

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 857	. 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 518	. 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  860  jaoi2OLD  955  cases  957  cador  1437  rexun  3533  rabun2  3626  reuun2  3630  xpundir  4888  coundi  5336  mptun  5538  tpostpos  6764  wemapsolem  7760  ltxr  11091  hashbclem  12201  hashf1lem2  12205  pythagtriplem2  13880  pythagtrip  13897  vdwapun  14031  legtrid  22977  colinearalg  23091  usgraedg4  23240  vdgrun  23506  vdgrfiun  23507  elimifd  25840  elim2if  25841  dfon2lem5  27529  nobndup  27770  nofulllem5  27776  seglelin  28076  cnambfre  28365  expdioph  29297